On pot, pans and pudding or how to discover generalised critical Pairs

DOI10.1007/3-540-58156-1_50zbMath1433.68539OpenAlexW1591350144MaRDI QIDQ5210806

Reinhard Bündgen

Publication date: 21 January 2020

Published in: Automated Deduction — CADE-12 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-58156-1_50

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Associative-commutative unification
• An algebraic approach to unification under associativity and commutativity
• Only prime superpositions need be considered in the Knuth-Bendix completion procedure
• Critical pair criteria for completion
• Termination and completion modulo associativity, commutativity and identity
• The diamond lemma for ring theory
• On theories with a combinatorial definition of 'equivalence'
• Completion of a Set of Rules Modulo a Set of Equations
• 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
• Complete sets of reductions modulo associativity, commutativity and identity
• On how to move mountains ‘associatively and commutatively’