Proof Certificates for Algebra and their Application to Automatic Geometry Theorem Proving - Archive ouverte HAL Access content directly
Book Sections Year : 2011

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

(1) , (1) , (1)
1
Benjamin Grégoire
Laurent Théry

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.

Dates and versions

hal-01112767 , version 1 (03-02-2015)

Identifiers

Cite

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⟩

Collections

INRIA INRIA2
87 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More