Completion for rewriting modulo a congruence

DOI10.1016/0304-3975(89)90003-0zbMath0686.68021MaRDI QIDQ1262752

Nachum Dershowitz, Leo Bachmair

Publication date: 1989

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(89)90003-0

zbMATH Keywords

reasoning; completion; equational inference; rewriting modulo a congruence

Mathematics Subject Classification ID

68W30: Symbolic computation and algebraic computation

68Q65: Abstract data types; algebraic specification

08B05: Equational logic, Mal'tsev conditions

Related Items

Towards a foundation of completion procedures as semidecision procedures, A rewriting strategy to verify observational congruence, Termination and completion modulo associativity, commutativity and identity, Automated deduction with associative-commutative operators, Partial completion of equational theories, Infinite complete group presentations

Uses Software

• REVE

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Termination of rewriting systems by polynomial interpretations and its implementation
• Refutational theorem proving using term-rewriting systems
• Termination orderings for associative-commutative rewriting systems
• Only prime superpositions need be considered in the Knuth-Bendix completion procedure
• Critical pair criteria for completion
• New decision algorithms for finitely presented commutative semigroups
• Complete sets of unifiers and matchers in equational theories
• Completion of a Set of Rules Modulo a Set of Equations
• Proving termination with multiset orderings
• 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