AC unification through order-sorted AC1 unification

DOI10.1007/3-540-53904-2_89zbMATH Open1503.68102OpenAlexW1820316515MaRDI QIDQ5055752FDOQ5055752

Authors Eric Domenjoud 

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-53904-2_89

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Mechanization of proofs and logical operations (03B35)

Recommendations

• AC unification through order-sorted AC1 unification
• Order-sorted unification
• scientific article; zbMATH DE number 4092822
• A precedence-based total AC-compatible ordering
• Order-sorted feature theory unification
• An ordering linear unification algorithm
• Extending reduction orderings to ACU-compatible reduction orderings
• Order-sorted equational unification revisited
• A total AC-compatible ordering based on RPO
• Unification in sort theories and its applications

Cites work

• scientific article; zbMATH DE number 3871322 (Why is no real title available?)
• scientific article; zbMATH DE number 4213327 (Why is no real title available?)
• scientific article; zbMATH DE number 4056995 (Why is no real title available?)
• scientific article; zbMATH DE number 176134 (Why is no real title available?)
• scientific article; zbMATH DE number 3995771 (Why is no real title available?)
• A Unification Algorithm for Associative-Commutative Functions
• AC unification through order-sorted AC1 unification
• Adventures in associative-commutative unification
• An algorithm to generate the basis of solutions to homogeneous linear Diophantine equations
• Complete sets of reductions modulo associativity, commutativity and identity
• Efficient solution of linear diophantine equations
• On solving equations and disequations
• Unification in a combination of arbitrary disjoint equational theories
• Unification in abelian semigroups

Cited in

(6)

• Competing for the \(AC\)-unification race
• AC unification through order-sorted AC1 unification
• Order-sorted unification
• Order-sorted equational unification revisited
• AC-complete unification and its application to theorem proving
• Extending reduction orderings to ACU-compatible reduction orderings

This page was built for publication: AC unification through order-sorted AC1 unification

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