Rewrite method for theorem proving in first order theory with equality
- 4 February 1987
- journal article
- Published by Elsevier in Journal of Symbolic Computation
- Vol. 3 (1-2) , 133-151
- https://doi.org/10.1016/s0747-7171(87)80024-x
Abstract
No abstract availableKeywords
This publication has 9 references indexed in Scilit:
- Procedure implementation through demodulation and related tricksPublished by Springer Nature ,2005
- Refutational theorem proving using term-rewriting systemsArtificial Intelligence, 1985
- Equational methods in first order predicate calculusJournal of Symbolic Computation, 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 supportPublished by Springer Nature ,1970