Only prime superpositions need be considered in the Knuth-Bendix completion procedure

DOI10.1016/S0747-7171(88)80019-1zbMath0651.68029MaRDI QIDQ1106657

Deepak Kapur, Paliath Narendran, David R. Musser

Publication date: 1988

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

Knuth-Bendix completioncritical pairChurch-Rosser propertyterm rewriting systemprime superpositions

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Abstract data types; algebraic specification (68Q65)

Related Items

A Lower Bound of the Number of Rewrite Rules Obtained by Homological Methods, On how to move mountains ‘associatively and commutatively’, Consider only general superpositions in completion procedures, AC-complete unification and its application to theorem proving, On proving termination by innermost termination, Confluence of terminating conditional rewrite systems revisited, Multi-completion with termination tools, A refutational approach to geometry theorem proving, Unnecessary inferences in associative-commutative completion procedures, Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties, Automated proofs of the Moufang identities in alternative rings, Redundancy criteria for constrained completion, Harald Ganzinger’s Legacy: Contributions to Logics and Programming, Noncommutative Gröbner Basis over a Divisible and Annihilable Ring, Redundancy criteria for constrained completion, AC Completion with Termination Tools, Associative-commutative deduction with constraints, On pot, pans and pudding or how to discover generalised critical Pairs, Completion for rewriting modulo a congruence, Extending Maximal Completion (Invited Talk), Automating inductionless induction using test sets, Multi-valued logic and Gröbner bases with applications to modal logic, Elimination of composite superpositions may cause abortion

Uses Software

• RRL
• REVE

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proof by consistency
• Non-resolution theorem proving
• Completion of a Set of Rules Modulo a Set of Equations
• Proving termination with multiset orderings
• Abstract Data Type Specification in the Affirm System
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• A Unification Algorithm for Associative-Commutative Functions
• Complete Sets of Reductions for Some Equational Theories
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity