Certified Gröbner bases computations
Laurent Théry , Loïc Pottier
CROAP project, INRIA Sophia Antipolis

This page gives certified implementations of Buchberger algorithm for Gröbner bases computations, running on Linux, Sun, and Dec platforms.

These programs are certified:
all algorithms have been written in the Coq system, have been proven to be correct, and by an automatic mechanism, their translations into ocaml programs have been produced, and then compiled into native code.

Description:
Three versions are provided:

Use:
The executable commands are gbcoq, gbcoq2, and gbcoq2int, used with the following syntax:

gbcoq -file <filename>

gbcoq2 -file <filename>

gbcoq2int -file <filename>

where the file <filename> contains a list of variables, and a list of polynomials, in a Maple-like syntax, for instance (cyclic5 problem):

[a,b,c,d,e]

[a*b*c*d*e - 1,
a*b*c*d + b*c*d*e + c*d*e*a + d*e*a*b + e*a*b*c,
a*b*c + b*c*d + c*d*e + d*e*a + e*a*b,
a*b + b*c + c*d + d*e + e*a,
a+b+c+d+e]

Download gbcoq (1456 K: ocaml sources and binaries for Linux, Dec , and Sun)

Browse the Coq Development

Benchs:
Here are some computation times on a PC 300MHz -128Meg:

gbcoq2 gbcoq2int gbcoq
cyclic 5 0.15s 0.31s 1.04s
cyclic 6 3.95s 61.71s 52.09s
cyclic 7 816.92s

References:

Laurent Théry,
``Proving and Computing: a certified version of the Buchberger's algorithm '',
Rapport de Recherche INRIA 3275, Octobre 1997.

Related works: