Additional Key Words and Phrases: automatic theorem proving, first order logic, resolution, completeness, ordering, merge, linear format, set of support
Selected papers that cite this one
- 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.
- D. W. Loveland. A unifying view of some linear Herbrand procedures. Journal of the ACM, 19(2):366-384, April 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.
- Peter B. Andrews. Resolution with merging. Journal of the ACM, 15(3):367-381, July 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.