Selected papers that cite this one
- Anatoli Degtyarev, Yuri Matiyasevich, and Andrei Voronkov. Simultaneous E-unification and related algorithmic problems. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, pages 494-502, New Brunswick, New Jersey, 27-30 July 1996. IEEE Computer Society Press.
- Anatoli Degtyarev and Andrei Voronkov. The undecidability of simultaneous rigid E-unification. Theoretical Computer Science, 166(1-2):291-300, 20 October 1996. Note.
- Anatoli Degtyarev and Andrei Voronkov. Decidability problems for the prenex fragment of intuitionistic logic. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, pages 503-512, New Brunswick, New Jersey, 27-30 July 1996. IEEE Computer Society Press.
- 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.
- Donald W. Loveland. Erratum: ``Mechanical theorem-proving by model elimination''. Journal of the ACM, 16(4):646, October 1969.
- D. W. Loveland. A unifying view of some linear Herbrand procedures. Journal of the ACM, 19(2):366-384, April 1972.
- D. W. Loveland. A simplified format for the model elimination theorem-proving procedure. Journal of the ACM, 16(3):349-363, July 1969.
- Christopher Lynch. Local simplification. Information and Computation, 142(1):102-126, 10 April 1998.
- Ross A. Overbeek. A new class of automated theorem-proving algorithms. Journal of the ACM, 21(2):191-200, April 1974.
- S. C. van Westrehnen. Statistical studies of theoremhood in classical propositional and first order predicate calculus. Journal of the ACM, 19(2):347-365, April 1972.
Selected references
- Joyce Friedman. A semi-decision procedure for the functional calculus. Journal of the ACM, 10(1):1-24, January 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.