AC-complete unification and its application to theorem proving

DOI10.1007/3-540-61464-8_40MaRDI QIDQ5055849zbMATH OpenOpenAlexFDO

Authors Alexandre Boudet, Evelyne Contejean, Claude Marché

Publication date 9 December 2022

Published in Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-61464-8_40

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 4043300
• Unification in abelian semigroups
• scientific article; zbMATH DE number 4074540
• AC unification through order-sorted AC1 unification
• AC unification through order-sorted AC1 unification

Cites work

• scientific article; zbMATH DE number 4089518 (Why is no real title available?)
• scientific article; zbMATH DE number 1348470 (Why is no real title available?)
• scientific article; zbMATH DE number 1348479 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• A Unification Algorithm for Associative-Commutative Functions
• AC unification through order-sorted AC1 unification
• AC-superposition with constraints: no AC-unifiers needed
• Algebraic simplification
• An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal
• Associative-commutative deduction with constraints
• Associative-commutative unification
• Combining unification algorithms
• Complete Sets of Reductions for Some Equational Theories
• Complete sets of reductions modulo associativity, commutativity and identity
• Completion for rewriting modulo a congruence
• Completion of a Set of Rules Modulo a Set of Equations
• Critical pair criteria for completion
• Normalized rewriting: An alternative to rewriting modulo a set of equations
• Only prime superpositions need be considered in the Knuth-Bendix completion procedure
• Termination and completion modulo associativity, commutativity and identity
• Unification in abelian semigroups

Cited in

(11)

• Superposition theorem proving for abelian groups represented as integer modules
• Verification of the Completeness of Unification Algorithms à la Robinson
• Path indexing for AC-theories
• A general refutational completeness result for an inference procedure based on associative-commutative unification
• Cancellative Abelian monoids and related structures in refutational theorem proving. I
• Term Rewriting and Applications
• Canonized Rewriting and Ground AC Completion Modulo Shostak Theories
• Superposition theorem proving for abelian groups represented as integer modules
• AC-superposition with constraints: no AC-unifiers needed
• scientific article; zbMATH DE number 6785324 (Why is no real title available?)
• Canonized rewriting and ground AC completion modulo Shostak theories: design and implementation

This page was built for publication: AC-complete unification and its application to theorem proving

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