Unification in abelian semigroups

DOI10.1007/BF00243791zbMath0637.68106OpenAlexW2000095830MaRDI QIDQ1098653

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

linear diophantine equationsabelian monoidscomplexity measureAC- 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)

Related Items

Unification in partially commutative semigroups, AC-complete unification and its application to theorem proving, An algebraic approach to unification under associativity and commutativity, Embedding Boolean expressions into logic programming, Unification in commutative idempotent monoids, Efficient solution of linear diophantine equations, Unification in commutative semigroups, Modular AC unification of higher-order patterns, “Syntactic” AC-unification, Avoiding slack variables in the solving of linear diophantine equations and inequations, Petri nets are monoids, A partial solution for D-unification based on a reduction to AC 1-unification, A semantic framework for open processes, Unification algorithms cannot be combined in polynomial time, Unification theory, AC-unification race: The system solving approach, implementation and benchmarks, AC unification through order-sorted AC1 unification, Adventures in associative-commutative unification, Unification problem in equational theories, Unification in permutative equational theories is undecidable, Unification algorithms cannot be combined in polynomial time.