AC-superposition with constraints: no AC-unifiers needed

DOI10.1007/3-540-58156-1_40MaRDI QIDQ5210796zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Paramodulation with built-in AC-theories and symbolic constraints
• Associative-commutative deduction with constraints
• AC-complete unification and its application to theorem proving
• Termination and completion modulo associativity, commutativity and identity
• A general refutational completeness result for an inference procedure based on associative-commutative unification

Cites work

• 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\)
• A total AC-compatible ordering based on RPO
• Any ground associative-commutative theory has a finite canonical system
• Automated deduction with associative-commutative operators
• Complete Sets of Reductions for Some Equational Theories
• Completion for rewriting modulo a congruence
• Completion of a Set of Rules Modulo a Set of Equations
• Complexity of unification problems with associative-commutative operators
• scientific article; zbMATH DE number 1348468 (Why is no real title available?)
• scientific article; zbMATH DE number 1348470 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• Rewrite-based Equational Theorem Proving with Selection and Simplification

Cited in

(17)

• Local simplification
• Superposition theorem proving for abelian groups represented as integer modules
• Paramodulation with built-in AC-theories and symbolic constraints
• Theorem proving modulo
• Cancellative Abelian monoids and related structures in refutational theorem proving. I
• AC simplifications and closure redundancies in the superposition calculus
• On the complexity of Boolean unification
• Proof-search in intuitionistic logic based on constraint satisfaction
• Theorem proving in cancellative abelian monoids (extended abstract)
• 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
• Superposition theorem proving for abelian groups represented as integer modules
• Local simplification
• Associative-commutative deduction with constraints
• Theorem proving modulo associativity
• A total AC-compatible ordering based on RPO

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5210796)