Completion for rewriting modulo a congruence
- 3 October 1989
- journal article
- Published by Elsevier in Theoretical Computer Science
- Vol. 67 (2-3) , 173-201
- https://doi.org/10.1016/0304-3975(89)90003-0
Abstract
No abstract availableKeywords
This publication has 17 references indexed in Scilit:
- Critical pair criteria for completionJournal of Symbolic Computation, 1988
- Only prime superpositions need be considered in the Knuth-Bendix completion procedureJournal of Symbolic Computation, 1988
- Termination of rewriting systems by polynomial interpretations and its implementationScience of Computer Programming, 1987
- Termination orderings for associative-commutative rewriting systemsJournal of Symbolic Computation, 1985
- Refutational theorem proving using term-rewriting systemsArtificial Intelligence, 1985
- 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
- Proving termination with multiset orderingsCommunications of the ACM, 1979
- Automated Theorem-Proving for Theories with Simplifiers Commutativity, and AssociativityJournal of the ACM, 1974