Proof Certificates for Algebra and their Application to Automatic Geometry Theorem Proving

Loïc Pottier 1, * Laurent Théry 1
* Auteur correspondant
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : Integrating decision procedures in proof assistants in a safe way is a major challenge. In this paper, we describe how, starting from Hilbert's Nullstellensatz theorem, we combine a modified version of Buchberger's algorithm and some reflexive techniques to get an effective procedure that automatically produces formal proofs of theorems in geometry. The method is implemented in the Coq system but, since our specialised version of Buchberger's algorithm outputs explicit proof certificates, it could be easily adapted to other proof assistants.
Type de document :
Communication dans un congrès
Thomas Sturm; Christoph Zengler. 7th International Workshop, ADG 2008, Sep 2008, Shangai, China. Springer, 7th International Workshop, ADG 2008, Shanghai, China, September 22-24, 2008. Revised Papers, 6301, pp.42-59, 2011, Lecture Notes in Computer Science. 〈10.1007/978-3-642-21046-4_3〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00504719
Contributeur : Loïc Pottier <>
Soumis le : mercredi 21 juillet 2010 - 11:29:49
Dernière modification le : jeudi 11 janvier 2018 - 16:21:46
Document(s) archivé(s) le : vendredi 22 octobre 2010 - 16:16:57

Fichier

pottier.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Loïc Pottier, Laurent Théry. Proof Certificates for Algebra and their Application to Automatic Geometry Theorem Proving. Thomas Sturm; Christoph Zengler. 7th International Workshop, ADG 2008, Sep 2008, Shangai, China. Springer, 7th International Workshop, ADG 2008, Shanghai, China, September 22-24, 2008. Revised Papers, 6301, pp.42-59, 2011, Lecture Notes in Computer Science. 〈10.1007/978-3-642-21046-4_3〉. 〈inria-00504719〉

Partager

Métriques

Consultations de la notice

297

Téléchargements de fichiers

200