Additional Key Words and Phrases: mechanical theorem proving, Herbrand proof procedure, liked conjunct, resolution, model elimination, matrix reduction procedure, linear resolution procedure
Selected papers that cite this one
- S. Fleisig, D. Loveland, A. K. Smiley III, and D. L. Yarmush. An implementation of the model elimination proof procedure. Journal of the ACM, 21(1):124-139, January 1974.
- Arthur J. Nevins. A human oriented logic for automatic theorem-proving. Journal of the ACM, 21(4):606-621, October 1974.
Selected references
- Robert Anderson and W. W. Bledsoe. A linear format for resolution with merging and a new technique for establishing completeness. Journal of the ACM, 17(3):525-534, July 1970.
- C. L. Chang. The unit proof and the input proof in theorem proving. Journal of the ACM, 17(4):698-707, October 1970.
- Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM, 7(3):201-215, July 1960.
- Donald W. Loveland. Mechanical theorem-proving by model elimination. Journal of the ACM, 15(2):236-251, April 1968.
- D. W. Loveland. A simplified format for the model elimination theorem-proving procedure. Journal of the ACM, 16(3):349-363, July 1969.
- Raymond Reiter. Two results on ordering for resolution with merging and linear format. Journal of the ACM, 18(4):630-646, October 1971.
- J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23-41, January 1965.
- James R. Slagle. Automatic theorem proving with renamable and semantic resolution. Journal of the ACM, 14(4):687-697, October 1967.