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

Loïc Pottier 1, * Laurent Théry 1
* Corresponding author
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.
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [28 references]  Display  Hide  Download

https://hal.inria.fr/inria-00504719
Contributor : Loïc Pottier <>
Submitted on : Wednesday, July 21, 2010 - 11:29:49 AM
Last modification on : Thursday, January 11, 2018 - 4:21:46 PM
Document(s) archivé(s) le : Friday, October 22, 2010 - 4:16:57 PM

File

pottier.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Loïc Pottier, Laurent Théry. Proof Certificates for Algebra and their Application to Automatic Geometry Theorem Proving. 7th International Workshop, ADG 2008, Sep 2008, Shangai, China. pp.42-59, ⟨10.1007/978-3-642-21046-4_3⟩. ⟨inria-00504719⟩

Share

Metrics

Record views

311

Files downloads

234