Selected papers that cite this one
- C. L. Chang. The unit proof and the input proof in theorem proving. Journal of the ACM, 17(4):698-707, October 1970.
- John K. Dixon. Z-resolution: Theorem-proving with compiled axioms. Journal of the ACM, 20(1):127-147, January 1973.
- Jieh Hsiang and Michaël Rusinowitch. Proving refutational completeness of theorem-proving strategies: The transfinite semantic tree method. Journal of the ACM, 38(3):559-587, July 1991.
- Richard B. Kieburtz and David Luckham. Compatibility and complexity of refinements of the resolution principle. SIAM Journal on Computing, 1(4):313-332, December 1972.
- D. W. Loveland. A unifying view of some linear Herbrand procedures. Journal of the ACM, 19(2):366-384, April 1972.
- Ross A. Overbeek. A new class of automated theorem-proving algorithms. Journal of the ACM, 21(2):191-200, April 1974.
- Nicolas Peltier. A new method for automated finite model building exploiting failures and symmetries. Journal of Logic and Computation, 8(4):511-543, August 1998.
- J. R. Quinlan and E. B. Hunt. A formal deductive problem-solving system. Journal of the ACM, 15(4):625-646, October 1968.
- Raymond Reiter. Two results on ordering for resolution with merging and linear format. Journal of the ACM, 18(4):630-646, October 1971.
- James R. Slagle. Automatic theorem proving with built-in theories including equality, partial ordering, and sets. Journal of the ACM, 19(1):120-135, January 1972.
- James R. Slagle. Interpolation theorems for resolution in lower predicate calculus. Journal of the ACM, 17(3):535-542, July 1970.
- James R. Slagle. An approach for finding C-linear complete inference systems. Journal of the ACM, 19(3):496-516, July 1972.
- 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.
Selected references
- Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM, 7(3):201-215, July 1960.
- J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23-41, January 1965.
- 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.