AC unification through order-sorted AC1 unification

DOI10.1007/3-540-53904-2_89MaRDI QIDQ5055752zbMATH OpenOpenAlexFDO

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

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

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

• 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
• 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?)
• On solving equations and disequations
• Unification in a combination of arbitrary disjoint equational theories
• Unification in abelian semigroups

Cited in

(7)

• AC unification through order-sorted AC1 unification
• Competing for the \(AC\)-unification race
• \({\mathsf{ACUOS}}^\mathbf{2}\): a high-performance system for modular ACU generalization with subtyping and inheritance
• Extending reduction orderings to ACU-compatible reduction orderings
• AC-complete unification and its application to theorem proving
• Order-sorted equational unification revisited
• Order-sorted unification

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)