Journal of the ACM Bibliography

Additional Key Words and Phrases: theorem proving, chain of reasoning, resolution, deduction, unit (input) proofs, subsumption tests, function-depth tests

Selected papers that cite this one

• C. L. Chang and J. R. Slagle. Completeness of linear refutation for theories with equality. Journal of the ACM, 18(1):126-136, January 1971.

• Marcello D'Agostino and Marco Mondadori. The taming of the cut. Classical refutations with analytic cut. Journal of Logic and Computation, 4(3):285-319, June 1994.

• L. Henschen and L. Wos. Unit refutations and Horn sets. Journal of the ACM, 21(4):590-605, October 1974.

• D. W. Loveland. A unifying view of some linear Herbrand procedures. Journal of the ACM, 19(2):366-384, April 1972.

• Arthur J. Nevins. A human oriented logic for automatic theorem-proving. Journal of the ACM, 21(4):606-621, October 1974.

• Ross A. Overbeek. A new class of automated theorem-proving algorithms. Journal of the ACM, 21(2):191-200, April 1974.

Selected references

• Peter B. Andrews. Resolution with merging. Journal of the ACM, 15(3):367-381, July 1968.

• Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM, 7(3):201-215, July 1960.

• J. R. Quinlan and E. B. Hunt. A formal deductive problem-solving system. Journal of the ACM, 15(4):625-646, October 1968.

• 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.

• Lawrence Wos, George A. Robinson, and Daniel F. Carson. Efficiency and completeness of the set of support strategy in theorem proving. Journal of the ACM, 12(4):536-541, October 1965.

• Lawrence Wos, George A. Robinson, Daniel F. Carson, and Leon Shalla. The concept of demodulation in theorem proving. Journal of the ACM, 14(4):698-709, October 1967.

Shortcuts: