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
Coghetto, Roland; Grabowski, Adam Tarski geometry axioms. II. (English) Zbl 1352.51001 Formaliz. Math. 24, No. 2, 157-166 (2016). MSC: 51A05 03B35 PDFBibTeX XMLCite \textit{R. Coghetto} and \textit{A. Grabowski}, Formaliz. Math. 24, No. 2, 157--166 (2016; Zbl 1352.51001) Full Text: DOI
Richter, William; Grabowski, Adam; Alama, Jesse Tarski geometry axioms. (English) Zbl 1352.51002 Formaliz. Math. 22, No. 2, 167-176 (2014). MSC: 51A05 03B35 PDFBibTeX XMLCite \textit{W. Richter} et al., Formaliz. Math. 22, No. 2, 167--176 (2014; Zbl 1352.51002) Full Text: DOI