Additional Key Words and Phrases: automatic theorem-proving, natural deduction, splitting, existential interpretation, associativity, resolution
Selected references
- C. L. Chang. The unit proof and the input proof in theorem proving. Journal of the ACM, 17(4):698-707, October 1970.
- George W. Ernst. The utility of independent subgoals in theorem proving. Information and Control, 18(3):237-252, April 1971.
- D. W. Loveland. A unifying view of some linear Herbrand procedures. Journal of the ACM, 19(2):366-384, April 1972.
- J. A. Robinson. Theorem-proving on the computer. Journal of the ACM, 10(2):163-174, April 1963.
- 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.