Unification in commutative theories, Hilbert’s basis theorem, and Gröbner bases.

*(English)*Zbl 0791.68146Given 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.

Reviewer: J.Avenhaus (Kaiserslautern)

##### 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 |