Beeson, Michael; Narboux, Julien; Wiedijk, Freek Proof-checking Euclid. (English) Zbl 07055783 Ann. Math. Artif. Intell. 85, No. 2-4, 213-257 (2019). MSC: 03B30 51M05 PDFBibTeX XMLCite \textit{M. Beeson} et al., Ann. Math. Artif. Intell. 85, No. 2--4, 213--257 (2019; Zbl 07055783) Full Text: DOI arXiv
Boutry, Pierre; Gries, Charly; Narboux, Julien; Schreck, Pascal Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq. (English) Zbl 1441.03011 J. Autom. Reasoning 62, No. 1, 1-68 (2019). Reviewer: Victor V. Pambuccian (Glendale) MSC: 03B30 03B35 51F05 51M05 03F55 68V15 PDFBibTeX XMLCite \textit{P. Boutry} et al., J. Autom. Reasoning 62, No. 1, 1--68 (2019; Zbl 1441.03011) Full Text: DOI HAL
Boutry, Pierre; Braun, Gabriel; Narboux, Julien Formalization of the arithmetization of Euclidean plane geometry and applications. (English) Zbl 1394.68349 J. Symb. Comput. 90, 149-168 (2019). MSC: 68T15 03B30 03B35 51M04 68W30 PDFBibTeX XMLCite \textit{P. Boutry} et al., J. Symb. Comput. 90, 149--168 (2019; Zbl 1394.68349) Full Text: DOI HAL
Braun, Gabriel; Narboux, Julien From Tarski to Hilbert. (English) Zbl 1397.03019 Ida, Tetsuo (ed.) et al., Automated deduction in geometry. 9th international workshop, ADG 2012, Edinburgh, UK, September 17–19, 2012. Revised selected papers. Berlin: Springer (ISBN 978-3-642-40671-3/pbk). Lecture Notes in Computer Science 7993. Lecture Notes in Artificial Intelligence, 89-109 (2013). MSC: 03B35 03B30 68T15 PDFBibTeX XMLCite \textit{G. Braun} and \textit{J. Narboux}, Lect. Notes Comput. Sci. 7993, 89--109 (2013; Zbl 1397.03019) Full Text: DOI HAL