Completion for rewriting modulo a congruence
From MaRDI portal
Publication:1262752
DOI10.1016/0304-3975(89)90003-0zbMath0686.68021OpenAlexW1589182689MaRDI 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
Symbolic computation and algebraic computation (68W30) Abstract data types; algebraic specification (68Q65) Equational logic, Mal'tsev conditions (08B05)
Related Items
Automated deduction with associative-commutative operators ⋮ Coherent confluence modulo relations and double groupoids ⋮ Decidability of confluence and termination of monadic term rewriting systems ⋮ Proving equational and inductive theorems by completion and embedding techniques ⋮ Simulating Buchberger's algorithm by Knuth-Bendix completion ⋮ Bi-rewriting, a term rewriting technique for monotonic order relations ⋮ Explicit substitutions with de bruijn's levels ⋮ AC-complete unification and its application to theorem proving ⋮ String Diagram Rewrite Theory I: Rewriting with Frobenius Structure ⋮ Infinite complete group presentations ⋮ Buchberger's algorithm: The term rewriter's point of view ⋮ On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories ⋮ A rewriting strategy to verify observational congruence ⋮ Towards a foundation of completion procedures as semidecision procedures ⋮ Strict coherence of conditional rewriting modulo axioms ⋮ Termination and completion modulo associativity, commutativity and identity ⋮ AC-superposition with constraints: No AC-unifiers needed ⋮ A completion-based method for mixed universal and rigid E-unification ⋮ Equational theorem proving modulo ⋮ Extending Maximal Completion (Invited Talk) ⋮ Termination Modulo Combinations of Equational Theories ⋮ Partial completion of equational theories ⋮ Deduction, Strategies, and Rewriting ⋮ Confluence of algebraic rewriting systems
Uses Software
Cites Work
- 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
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
