Proving refutational completeness of theorem-proving strategies
- 1 July 1991
- journal article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 38 (3) , 558-586
- https://doi.org/10.1145/116825.116833
Abstract
In this paper, a proof method based on a notion of transfinite semantic trees is presented and it is shown how to apply it to prove the completeness of refutational theorem proving methods for first order predicate calculus with equality. To demonstrate how this method is used, the completeness of two theorem-proving strategies, both refinements of resolution and paramodulation, are proved. Neither of the strategies need the functionally reflexive axioms nor paramodulating into variables. Therefore the Wos-Robinson conjecture follows as a corollary. Another strategy for Horn logic with equality is also presented.Keywords
This publication has 17 references indexed in Scilit:
- Termination of rewritingJournal of Symbolic Computation, 1987
- On word problems in equational theoriesPublished by Springer Nature ,1987
- A superposition oriented theorem proverTheoretical Computer Science, 1985
- Orderings for term-rewriting systemsTheoretical Computer Science, 1982
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting SystemsJournal of the ACM, 1980
- 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
- Unit Refutations and Horn SetsJournal of the ACM, 1974
- Refinement theorems in resolution theoryPublished by Springer Nature ,1970