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

Benjamin Grégoire 1 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.
Keywords : geometry theorem proving Nullstellensatz decision procedure proof assistant
Type de document :
Chapitre d'ouvrage
Thomas Sturm; Christoph Zengler. Automated Deduction in Geometry, 6301, Springer, pp.42-59, 2011, Lecture Notes in Computer Science, 978-3-642-21045-7. 〈10.1007/978-3-642-21046-4_3〉
Liste complète des métadonnées
https://hal.inria.fr/hal-01112767
Contributeur : Alain Monteil <>
Soumis le : mardi 3 février 2015 - 15:58:41
Dernière modification le : jeudi 11 janvier 2018 - 16:22:57

Identifiants

Collections

INRIA | UNIV-COTEDAZUR

Relations

Citation

Benjamin Grégoire, Loïc Pottier, Laurent Théry. Proof Certificates for Algebra and their Application to Automatic Geometry Theorem Proving. Thomas Sturm; Christoph Zengler. Automated Deduction in Geometry, 6301, Springer, pp.42-59, 2011, Lecture Notes in Computer Science, 978-3-642-21045-7. 〈10.1007/978-3-642-21046-4_3〉. 〈hal-01112767〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

146

Contact


archive-ouverte@inria.fr