Only prime superpositions need be considered in the Knuth-Bendix completion procedure
Open Access
- 1 August 1988
- journal article
- Published by Elsevier in Journal of Symbolic Computation
- Vol. 6 (1) , 19-36
- https://doi.org/10.1016/s0747-7171(88)80019-1
Abstract
No abstract availableKeywords
This publication has 8 references indexed in Scilit:
- Proof by consistencyArtificial Intelligence, 1987
- A Unification Algorithm for Associative-Commutative FunctionsJournal of the ACM, 1981
- Complete Sets of Reductions for Some Equational TheoriesJournal of the ACM, 1981
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting SystemsJournal of the ACM, 1980
- Abstract Data Type Specification in the Affirm SystemIEEE Transactions on Software Engineering, 1980
- Proving termination with multiset orderingsCommunications of the ACM, 1979
- Non-resolution theorem provingArtificial Intelligence, 1977
- Automated Theorem-Proving for Theories with Simplifiers Commutativity, and AssociativityJournal of the ACM, 1974