Additional Key Words and Phrases: theorem-proving, efficiency, resolution principle, paramodulation, refutation completeness, unification algorithm, inference rules, artificial intelligence, mathematical logic, predicate calculus, left and right identity, commutativity, associativity, simplifiers, simplification
Selected papers that cite this one
- Leo Bachmair, Harald Ganzinger, Christopher Lynch, and Wayne Snyder. Basic paramodulation. Information and Computation, 121(2):172-192, September 1995.
- 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.
- Tetsuo Ida and Koichi Nakahara. Leftmost outside-in narrowing calculi Journal of Functional Programming, 7(2):129-161, March 1997
- Aart Middeldorp, Satoshi Okui, and Tetsuo Ida. Lazy narrowing: Strong completeness and eager variable elimination. Theoretical Computer Science, 167(1-2):95-130, 30 October 1996.
Selected references
- J. R. Guad, F. C. Oglesby, J. H. Bennett, and L. G. Settle. Semi-automated mathematics. Journal of the ACM, 16(1):49-62, January 1969.
- James R. Slagle. Automatic theorem proving with built-in theories including equality, partial ordering, and sets. Journal of the ACM, 19(1):120-135, January 1972.
- James R. Slagle. An approach for finding C-linear complete inference systems. Journal of the ACM, 19(3):496-516, July 1972.
- 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.
- Lawrence Wos, George A. Robinson, Daniel F. Carson, and Leon Shalla. The concept of demodulation in theorem proving. Journal of the ACM, 14(4):698-709, October 1967.