Skip to content
Proof of Buchberger's algorithm
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
.gitignore Renaming ".cvsignore" to ".gitignore" Apr 11, 2016
Bar.v
Buch.v
BuchAux.v avoid the use of undocumented and obsolete tactic specialize Mar 5, 2008
BuchRed.v Fixing Buchberger. May 1, 2014
CoefStructure.v Licence pour les contribs May 24, 2006
Dickson.v
DivTerm.v Licence pour les contribs May 24, 2006
Extract.v
Fred.v
LICENSE
LetP.v Licence pour les contribs May 24, 2006
LexiOrder.v
ListProps.v Licence pour les contribs May 24, 2006
Make CLEANUP: "Make" file Mar 15, 2016
Makefile Makefile: no more message about a Circular Make <- Makefile.coq depen… Jun 24, 2016
Monomials.v Licence pour les contribs May 24, 2006
OpenIndGoodRel.v Licence pour les contribs May 24, 2006
OrderStructure.v
POrder.v
Pcomb.v
Pcrit.v Licence pour les contribs May 24, 2006
Peq.v
Pminus.v
Pmult.v Licence pour les contribs May 24, 2006
Pmults.v
Pplus.v Licence pour les contribs May 24, 2006
Preduce.v
Preduceplus.v Licence pour les contribs May 24, 2006
Preducestar.v
Pspminus.v Licence pour les contribs May 24, 2006
Pspoly.v Licence pour les contribs May 24, 2006
README Initial revision Mar 29, 2004
Relation_Operators_compat.v Fixing Buchberger by violently adding the old definitions. Sep 19, 2013
Term.v Licence pour les contribs May 24, 2006
WfR0.v
description Converting from iso-8859-1 to utf8. Oct 20, 2018
hBuch.v Licence pour les contribs May 24, 2006
hBuchAux.v
hCoefStructure.v
hComb.v Licence pour les contribs May 24, 2006
hEq.v
hMinus.v Licence pour les contribs May 24, 2006
hMult.v Licence pour les contribs May 24, 2006
hMults.v
hOrder.v Licence pour les contribs May 24, 2006
hOrderStructure.v Licence pour les contribs May 24, 2006
hPlus.v Licence pour les contribs May 24, 2006
hReduce.v
hReduceplus.v Licence pour les contribs May 24, 2006
hReducestar.v
hSpminus.v
hSpoly.v Licence pour les contribs May 24, 2006
hTerm.v Licence pour les contribs May 24, 2006
hWfRO.v
mCoefStructure.v
mOrderStructure.v Licence pour les contribs May 24, 2006
moreCoefStructure.v
run.ml

README

This directory contains the formalization of Buchberger's algorithm.


It is composed of :

-  A proof of correctness of the algorithm as described in 
    `A machine checked implementation of Buchberger's algorithm' in JAR Jan. 
2001.

- An implementation of the algorithm. With respect to the paper,
  terms are not abstracted but built directly from coef and monomials.

- A constructive proof of Dickson's lemma due to Henrik Persson

To build the directory, do

  coq_makefile *.v > Makefile

Then

  make depend;make all
  
In Extract.v we explain how the extracted code produced in
the file sin_num.ml can be used to compute Grobner basis.

 Laurent Thery            Henrik Persson                      
 thery@sophia.inria.fr    Henrik.Persson@prover.com
You can’t perform that action at this time.