Unification in abelian semigroups

DOI10.1007/BF00243791MaRDI QIDQ1098653zbMATH OpenOpenAlexFDO

Authors Alexander Herold, Jörg H. Siekmann

Publication date 1987

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf00243791

zbMATH Keywords

abelian monoidscomplexity measurelinear diophantine equationsAC- unificationassociative-communicative theoriesconstant abstraction

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Semigroups in automata theory, linguistics, etc. (20M35) Linear Diophantine equations (11D04)

Recommendations

• scientific article; zbMATH DE number 4074540
• scientific article; zbMATH DE number 3871322
• “Syntactic” AC-unification
• An algebraic approach to unification under associativity and commutativity
• Associative-commutative unification

Cited in

(32)

• AC-complete unification and its application to theorem proving
• Unification algorithms cannot be combined in polynomial time.
• Unification in commutative semigroups
• Avoiding slack variables in the solving of linear diophantine equations and inequations
• An algebraic approach to unification under associativity and commutativity
• scientific article; zbMATH DE number 4043300 (Why is no real title available?)
• Unification theory
• Adventures in associative-commutative unification
• Unification algorithms cannot be combined in polynomial time
• scientific article; zbMATH DE number 3871322 (Why is no real title available?)
• Unification in partially commutative semigroups
• A semantic framework for open processes
• Petri nets are monoids
• Constraint solving for term orderings compatible with abelian semigroups, monoids and groups
• scientific article; zbMATH DE number 3885353 (Why is no real title available?)
• Unification in commutative idempotent monoids
• Unification modulo ACUI plus homomorphisms/distributivity.
• Embedding Boolean expressions into logic programming
• AC unification through order-sorted AC1 unification
• AC unification through order-sorted AC1 unification
• Efficient solution of linear diophantine equations
• Unification in permutative equational theories is undecidable
• Semi-unification of two terms in Abelian groups
• Cancellative Abelian monoids and related structures in refutational theorem proving. II
• A partial solution for D-unification based on a reduction to AC1-unification
• 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\)
• AC-unification race: The system solving approach, implementation and benchmarks
• “Syntactic” AC-unification
• Modular AC unification of higher-order patterns
• Unification in commutative theories, Hilbert's basis theorem, and Gröbner bases
• A formally verified solver for homogeneous linear Diophantine equations
• Unification problem in equational theories

This page was built for publication: Unification in abelian semigroups

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