Journal of the ACM Bibliography

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.

Shortcuts: