Categories and Subject Descriptors: F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic -- mechanical theorem proving, proof theory; I.2.3 [Artificial Intelligence]: Deduction and Theorem Proving -- deduction, resolution
General Terms: Theory
Additional Key Words and Phrases: Refutational Theorem Proving Strategies, Transfinite Ordinals, Transfinite Semantic Trees, Resolution, Complete simplification orderings, completeness, first-order logic with equality, functional reflexive axioms, paramodulation, resolution, transfinite ordinals, transfinite semantic trees
Selected papers that cite this one
- Leo Bachmair and Harald Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217-247, June 1994.
- Leo Bachmair, Harald Ganzinger, Christopher Lynch, and Wayne Snyder. Basic paramodulation. Information and Computation, 121(2):172-192, September 1995.
- Adel Bouhoula, Emmanuel Kounalis, and Michaël Rusinowitch. Automated mathematical induction. Journal of Logic and Computation, 5(5):631-668, October 1995.
- Christopher Lynch. Local simplification. Information and Computation, 142(1):102-126, 10 April 1998.
Selected references
- L. Henschen and L. Wos. Unit refutations and Horn sets. Journal of the ACM, 21(4):590-605, October 1974.
- Gérard Huet. Confluent reductions: Abstract properties and application to term rewriting systems. Journal of the ACM, 27(4):797-821, October 1980.
- William H. Joyner Jr. Resolution strategies as decision procedures. Journal of the ACM, 23(3):398-417, July 1976.
- Raymond Reiter. Two results on ordering for resolution with merging and linear format. Journal of the ACM, 18(4):630-646, October 1971.
- James R. Slagle. Automatic theorem proving with renamable and semantic resolution. Journal of the ACM, 14(4):687-697, October 1967.
- James R. Slagle. Automated theorem-proving for theories with simplifiers, commutativity, and associativity. Journal of the ACM, 21(4):622-642, October 1974.
- 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.