Unification in abelian semigroups
DOI10.1007/BF00243791zbMATH Open0637.68106OpenAlexW2000095830MaRDI QIDQ1098653FDOQ1098653
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
Recommendations
abelian monoidscomplexity measurelinear diophantine equationsAC- unificationassociative-communicative theoriesconstant abstraction
Mechanization of proofs and logical operations (03B35) Semigroups in automata theory, linguistics, etc. (20M35) Linear Diophantine equations (11D04)
Cited In (30)
- Unification algorithms cannot be combined in polynomial time.
- Unification in commutative semigroups
- Avoiding slack variables in the solving of linear diophantine equations and inequations
- Unification theory
- Title not available (Why is that?)
- An algebraic approach to unification under associativity and commutativity
- Adventures in associative-commutative unification
- A partial solution for D-unification based on a reduction to AC 1-unification
- Unification algorithms cannot be combined in polynomial time
- Title not available (Why is that?)
- 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
- Title not available (Why is that?)
- Unification in commutative idempotent monoids
- 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 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
- Unification problem in equational theories
- AC-complete unification and its application to theorem proving
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)
