AC-superposition with constraints: No AC-unifiers needed

DOI10.1007/3-540-58156-1_40zbMath1433.68559OpenAlexW28083723MaRDI QIDQ5210796

Robert Nieuwenhuis, Albert Rubio

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_40

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (13)

On the complexity of Boolean unification ⋮ On narrowing, refutation proofs and constraints ⋮ Combination of constraint solving techniques: An algebraic point of view ⋮ AC-complete unification and its application to theorem proving ⋮ Theorem proving modulo ⋮ A total AC-compatible ordering based on RPO ⋮ Proof-search in intuitionistic logic based on constraint satisfaction ⋮ Theorem proving in cancellative abelian monoids (extended abstract) ⋮ Superposition theorem proving for abelian groups represented as integer modules ⋮ Local simplification ⋮ Superposition theorem proving for abelian groups represented as integer modules ⋮ Local simplification ⋮ Cancellative Abelian monoids and related structures in refutational theorem proving. I

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A total AC-compatible ordering based on RPO
• Complexity of unification problems with associative-commutative operators
• A technical note on AC-unification. The number of minimal unifiers of the equation \(\alpha x_ 1+ \cdots + \alpha x_ p \doteq _{AC} \beta y_ 1+ \cdots + \beta y_ q\)
• Completion for rewriting modulo a congruence
• Automated deduction with associative-commutative operators
• Any ground associative-commutative theory has a finite canonical system
• Completion of a Set of Rules Modulo a Set of Equations
• Complete Sets of Reductions for Some Equational Theories
• Rewrite-based Equational Theorem Proving with Selection and Simplification

This page was built for publication: AC-superposition with constraints: No AC-unifiers needed