Using forcing to prove completeness of resolution and paramodulation
- 28 February 1991
- journal article
- Published by Elsevier in Journal of Symbolic Computation
- Vol. 11 (1-2) , 3-19
- https://doi.org/10.1016/s0747-7171(08)80130-7
Abstract
No abstract availableKeywords
This publication has 9 references indexed in Scilit:
- Proving refutational completeness of theorem-proving strategiesJournal of the ACM, 1991
- Theorem-proving with resolution and superpositionJournal of Symbolic Computation, 1991
- Termination of rewritingJournal of Symbolic Computation, 1987
- 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
- Proving Theorems with the Modification MethodSIAM Journal on Computing, 1975
- Completing theories by forcingAnnals of Mathematical Logic, 1970
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965