Grégoire, Benjamin; Pottier, Loïc; Théry, Laurent Proof certificates for algebra and their application to automatic geometry theorem proving. (English) Zbl 1302.68242 Sturm, Thomas (ed.) et al., Automated deduction in geometry. 7th international workshop, ADG 2008, Shanghai, China, September 22–24, 2008. Revised papers. Berlin: Springer (ISBN 978-3-642-21045-7/pbk). Lecture Notes in Computer Science 6301. Lecture Notes in Artificial Intelligence, 42-59 (2011). Summary: 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.For the entire collection see [Zbl 1214.68020]. Cited in 8 Documents MSC: 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 13P10 Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) Keywords:decision procedure; Nullstellensatz; geometry theorem proving; proof assistant Software:GeoGebra; Maple; FGb; Coq; Isabelle; HOL Light; Macaulay2 PDFBibTeX XMLCite \textit{B. Grégoire} et al., Lect. Notes Comput. Sci. 6301, 42--59 (2011; Zbl 1302.68242) Full Text: DOI Link