Groebner bases over the integers

Hi,

I'm currently working with computations in the ring Z[X1...Xn] of
integer polynomials over finitely many variables (as a method for
handling non-linear arithmetic in a theorem prover). The problems that
we are dealing with usually (or often) have the shape

f1(X1,...,Xn)=0, ..., fk(X1,...,Xn)=0 |- g(X1,...,Xn)=0

where f1, ..., fx, g are polynomials over the integers. I.e., we want
to prove that whenever the functions that are described through
polynomials f1, ..., fk disappear for integers X1,...,Xn, also the
function described by g disappears. From Hilbert's 10th problem it is
clear that this problem is not decidable, but for practical purposes we
found that proofs often can be found by computing a Groebner basis of
f1, ..., fk and reducing g. Therefore, I am using the version of the
Buchberger algorithm that is described in "A Critical-Pair Completion
Algorithm for Finitely Generated Ideals in Rings", Buchberger, 1983.

That problem that I now have is: I want to complete the ideal
(f1,...,fk) by adding all polynomials that can be obtained by
eliminating common integer coefficients. As an example, in the
situation

2*x-2*y=0 |- x-y=0

I would in some way like to eliminate the "2" on the left side.
Likewise (and a bit more difficult), I also would like to be able to
prove

2*x+a=0, 2*y+a=0 |- x-y=0

More precisely, given an ideal I within Z[X1...Xn], I want to construct
a Groebner basis of the ideal I', where I' is the smallest ideal
containing I with the property: if a polynomial k*f is in I' (k a
non-zero integer), then also f is in I'

Unfortunately, so far I have no clue how I can compute such a basis
effectively ... but I seems to be a rather simple problem, so I would
be very grateful if someone in this group could tell me how to solve it
(or maybe tell about literature).

Thanks, Philipp

.

Relevant Pages

  • Re: Prime ideals of C[x]?
    ... The polynomials of degree at most m-1 ... | But what are ideals of this ring? ... |are prime ideals in this ring? ...
    (sci.math)
  • Re: Groebner basis question.
    ... Groebner basis exceeds the original number of polynomials. ... same set of roots does not in general give you that the ideals ... You can view each generating polynomials as rewrite rule, ...
    (sci.math)
  • Re: Yet another ideal problem
    ... > without assuming that our working ring had unity, ... > If I have an ideals I,J of a ring R, by IJ we mean *the ideal generated ... > this if the ring had no unity. ... Consider, for example, the ring of all polynomials without constant ...
    (sci.math)
  • Re: What is an primary ideal?
    ... if the ideal P in the ring R can be expressed as ... for some element p of R. If R is commutative, left and right ideals are ... the ring of polynomials over a field. ... single element. ...
    (sci.math)
  • Re: Maximal Ideals of Polynomial Rings
    ... > finite number of maximal left ideals!? ... If S=R/I is a quotient ring of R, for some two sided ideal I of R, ... Let P be a non-constant polynomials in F. ...
    (sci.math.research)