Additional Key Words and Phrases: automatic theorem-proving, Hergrand's theorem, predicate calculus
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.
- D. W. Loveland. A unifying view of some linear Herbrand procedures. Journal of the ACM, 19(2):366-384, April 1972.
Selected references
- Donald W. Loveland. Mechanical theorem-proving by model elimination. Journal of the ACM, 15(2):236-251, April 1968.
- J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23-41, January 1965.