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.

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: DOI