Additional Key Words and Phrases: theorem-proving, resolution, paramodulation, $E$-unsatisfiable sets, unit, input, linear refutations, functionally reflexive axioms, first-order logic with equality, set of support, unit factors
Selected papers that cite this one
- James R. Slagle. An approach for finding C-linear complete inference systems. Journal of the ACM, 19(3):496-516, July 1972.
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.
- 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 and Philip Bursky. Experiments with a multipurpose, theorem-proving heuristic program. Journal of the ACM, 15(1):85-99, January 1968.