Rewrite method for theorem proving in first order theory with equality
Author:
- 4 February 1987
- journal article
- Published by Elsevier in Journal of Symbolic Computation
- Vol. 3 (1-2) , 133-151
Abstract
No abstract availableKeywords
This publication has 8 references indexed in Scilit:
- Equational methods in first order predicate calculusJournal of Symbolic Computation, 1985
- Refutational theorem proving using term-rewriting systemsArtificial Intelligence, 1985
- A Technique for Establishing Completeness Results in Theorem Proving with EqualitySIAM Journal on Computing, 1983
- Orderings for term-rewriting systemsTheoretical Computer Science, 1982
- A complete proof of correctness of the Knuth-Bendix completion algorithmJournal of Computer and System Sciences, 1981
- Proving Theorems with the Modification MethodSIAM Journal on Computing, 1975
- Automated Theorem-Proving for Theories with Simplifiers Commutativity, and AssociativityJournal of the ACM, 1974
- Paramodulation and set of support1970