Version française
Home     About     Download     Resources     Contact us    
Browse thread
Is Grobner Basis calculation implemented in OCaml?
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Harrison, John R <john.r.harrison@i...>
Subject: RE: [Caml-list] Is Grobner Basis calculation implemented in OCaml?
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.