Proof Certificates for Algebra and their Application to Automatic Geometry Theorem Proving - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2011

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

Résumé

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.
Fichier principal
Vignette du fichier
pottier.pdf (199.38 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00504719 , version 1 (21-07-2010)

Identifiants

Citer

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⟩

Collections

INRIA INRIA2
154 Consultations
337 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More