Hi Guanhua,

| Does anyone know whether there is a library implemented to calculate
| Grobner Basis in OCaml? If there is, could you tell me where can I
find
| it, please?

There is a simple implementation here:

  http://www.cl.cam.ac.uk/~jrh13/atp/OCaml/grobner.ml

However this is a *very* straightforward version, just designed to
explain the algorithm rather than to be useful for serious problems.
It relies on some other code in the same directory (go up a bit to
"http://www.cl.cam.ac.uk/~jrh13/atp/" for more information) but the
dependencies are not that great and it would be quite easy to
separate.

There is a somewhat better implementation available as part of the
HOL Light prover (also available from my home page as above), which is
in a similar style and could also be ripped out without much effort.
It's better in that it uses Buchberger's first and second criteria for
ignoring S-polynomials, and also queues the S-polynomials in a
reasonable heuristic order.

John.