Armand, Michael; Faure, Germain; Grégoire, Benjamin; Keller, Chantal; Théry, Laurent; Werner, Benjamin A modular integration of SAT/SMT solvers to Coq through proof witnesses. (English) Zbl 1350.68223 Jouannaud, Jean-Pierre (ed.) et al., Certified programs and proofs. First international conference, CPP 2011, Kenting, Taiwan, December 7–9, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-25378-2/pbk). Lecture Notes in Computer Science 7086, 135-150 (2011). MSC: 68T15 PDFBibTeX XMLCite \textit{M. Armand} et al., Lect. Notes Comput. Sci. 7086, 135--150 (2011; Zbl 1350.68223) Full Text: DOI
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). MSC: 68T15 13P10 PDFBibTeX XMLCite \textit{B. Grégoire} et al., Lect. Notes Comput. Sci. 6301, 42--59 (2011; Zbl 1302.68242) Full Text: DOI Link