Proof normalization for resolution and paramodulation
- 1 January 1989
- book chapter
- Published by Springer Nature
Abstract
No abstract availableKeywords
This publication has 11 references indexed in Scilit:
- Termination of rewritingJournal of Symbolic Computation, 1987
- A new method for establishing refutational completeness in theorem provingPublished by Springer Nature ,1986
- A Technique for Establishing Completeness Results in Theorem Proving with EqualitySIAM Journal on Computing, 1983
- Orderings for term-rewriting systemsTheoretical Computer Science, 1982
- Proving termination with multiset orderingsCommunications of the ACM, 1979
- Resolution Strategies as Decision ProceduresJournal of the ACM, 1976
- Proving Theorems with the Modification MethodSIAM Journal on Computing, 1975
- Automated Theorem-Proving for Theories with Simplifiers Commutativity, and AssociativityJournal of the ACM, 1974
- The Concept of Demodulation in Theorem ProvingJournal of the ACM, 1967
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965