| HAL-Inria | Publications, software ... of Inria's scientists |
Book sections
Proof Certificates for Algebra and their Application to Automatic Geometry Theorem Proving
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.
https://hal.inria.fr/hal-01112767
Contributor : Alain Monteil Connect in order to contact the contributor
Submitted on : Tuesday, February 3, 2015 - 3:58:41 PM
Last modification on : Thursday, January 20, 2022 - 5:30:45 PM
Contributor : Alain Monteil Connect in order to contact the contributor
Submitted on : Tuesday, February 3, 2015 - 3:58:41 PM
Last modification on : Thursday, January 20, 2022 - 5:30:45 PM
Links full text
