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 (24)

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 ⋮ Left-Linear Completion with AC Axioms ⋮ 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

This page was built for publication: Only prime superpositions need be considered in the Knuth-Bendix completion procedure