Journal of the ACM Bibliography
James R. Slagle. Automated
theorem-proving for theories with simplifiers, commutativity, and
associativity. Journal of the ACM, 21(4):622-642, October
1974.
[BibTeX entry]
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.
Shortcuts: