# zbMATH — the first resource for mathematics

Unification in commutative theories, Hilbert’s basis theorem, and Gröbner bases. (English) Zbl 0791.68146
Given a set $$E$$ of equations, the $$E$$-unification problem is to solve equations modulo $$E$$, i.e., for an input $$\Gamma=\langle s_ i=t_ i\mid i=1,\ldots,n\rangle$$ one wants to compute a description of the set of solution $$U(\Gamma)=\{\sigma\mid s_ i\sigma=_ E t_ i\sigma,i=1,\ldots,n\}$$. A common approach is to do this syntactically, i.e., by using the equations in $$E$$ only. In the paper, for commutative theories this is replaced by a more semantic approach, i.e. by reasoning in a certain algebra: For a commutative theory $$E$$ the $$E$$-unification problem can be reduced to solving linear equations in a certain semiring $$S(E)$$. From properties of $$S(E)$$ one can conclude whether the $$E$$- unification problem is unitary, finitary, infinitary or of type zero. Even more, solving equations in $$S(E)$$ leads to computing a set $$cU(\Gamma)$$ of most general solutions of $$\Gamma$$. In the paper this is done for several theories, e.g., the theories $$AGnHC$$ and $$AGnH$$ of Abelian groups with $$n$$ commuting (respectively non-commuting) homomorphisms. In this case the semiring $$S(E)$$ is isomorphic to the ring $${\mathbb{Z}}[X_ 1,\ldots,X_ n]$$ (respectively $${\mathbb{Z}}\langle X_ 1,\ldots,X_ n\rangle$$) of $$n$$ commuting (respectively non-commuting) indeterminates over the integers. Now, solving the $$E$$-unification problem amounts to solving linear equations over these rings. For the latter problem algorithms are presented in the paper; they are based on Buchberger’s algorithm for computing Gröbner bases.

##### MSC:
 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 13P10 Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) 68W30 Symbolic computation and algebraic computation 03B35 Mechanization of proofs and logical operations
Full Text: