Connecting Gröbner Bases Programs with Coq to do Proofs in Algebra, Geometry and Arithmetics

Loïc Pottier 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : We describe how we connected three programs that compute Groebner bases to Coq, to do automated proofs on algebraic, geometrical and arithmetical expressions. The result is a set of Coq tactics and a certificate mechanism (downloadable at http://www-sop.inria.fr/marelle/Loic.Pottier/gb-keappa.tgz). The programs are: F4, GB \, and gbcoq. F4 and GB are the fastest (up to our knowledge) available programs that compute Groebner bases. Gbcoq is slow in general but is proved to be correct (in Coq), and we adapted it to our specific problem to be efficient. The automated proofs concern equalities and non-equalities on polynomials with coefficients and indeterminates in R or Z, and are done by reducing to Groebner computation, via Hilbert's Nullstellensatz. We adapted also the results of Harrison, to allow to prove some theorems about modular arithmetics. The connection between Coq and the programs that compute Groebner bases is done using the "external" tactic of Coq that allows to call arbitrary programs accepting xml inputs and outputs. We also produce certificates in order to make the proof scripts independant from the external programs.
Type de document :
Communication dans un congrès
Sutcliffe, G. and Rudnicki, P. and Schmidt, R. and Konev, B. and Schulz, S. Knowledge Exchange: Automated Provers and Proof Assistants, Nov 2008, Doha, Qatar. pp.418, 2008, CEUR Workshop Proceedings
Liste complète des métadonnées

Littérature citée [9 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00504727
Contributeur : Loïc Pottier <>
Soumis le : mercredi 21 juillet 2010 - 12:54:58
Dernière modification le : jeudi 11 janvier 2018 - 16:41:47
Document(s) archivé(s) le : vendredi 22 octobre 2010 - 16:24:26

Fichiers

easychair-a4.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00504727, version 1
  • ARXIV : 1007.3615

Collections

Citation

Loïc Pottier. Connecting Gröbner Bases Programs with Coq to do Proofs in Algebra, Geometry and Arithmetics. Sutcliffe, G. and Rudnicki, P. and Schmidt, R. and Konev, B. and Schulz, S. Knowledge Exchange: Automated Provers and Proof Assistants, Nov 2008, Doha, Qatar. pp.418, 2008, CEUR Workshop Proceedings. 〈inria-00504727〉

Partager

Métriques

Consultations de la notice

307

Téléchargements de fichiers

725