| The area method: a recapitulation P Janicic, J Narboux, P Quaresma Journal of Automated Reasoning 48 (4), 489-532, 2012 | 81 | 2012 |
| A graphical user interface for formal proofs in geometry J Narboux Journal of Automated Reasoning 39 (2), 161-180, 2007 | 73 | 2007 |
| Mechanical theorem proving in Tarski’s geometry J Narboux Automated Deduction in Geometry, 139-156, 2007 | 72 | 2007 |
| A decision procedure for geometry in coq J Narboux Theorem Proving in Higher Order Logics, 33-62, 2004 | 61 | 2004 |
| From Tarski to Hilbert G Braun, J Narboux Automated Deduction in Geometry: 9th International Workshop, ADG 2012 …, 2013 | 46 | 2013 |
| The Area Method P Janičić, J Narboux, P Quaresma Journal of Automated Reasoning, 1-44, 2012 | 41 | 2012 |
| Formalizing projective plane geometry in Coq N Magaud, J Narboux, P Schreck Automated Deduction in Geometry, 141-162, 2011 | 36 | 2011 |
| Formalization of Wu’s simple method in Coq JD Génevaux, J Narboux, P Schreck Certified Programs and Proofs, 71-86, 2011 | 32 | 2011 |
| Formalisation et automatisation du raisonnement géométrique en Coq. J Narboux Université Paris Sud-Paris XI, 2006 | 31 | 2006 |
| Automated generation of machine verifiable and readable proofs: a case study of Tarski’s geometry SS Ðurđević, J Narboux, P Janičić Annals of Mathematics and Artificial Intelligence 74 (3-4), 249-269, 2015 | 27 | 2015 |
| Formalizing Desargues' theorem in Coq using ranks N Magaud, J Narboux, P Schreck Proceedings of the 2009 ACM symposium on Applied Computing, 1110-1115, 2009 | 27 | 2009 |
| Using small scale automation to improve both accessibility and readability of formal proofs in geometry P Boutry, J Narboux, P Schreck, G Braun Automated Deduction in Geometry 2014, 1-19, 2014 | 26 | 2014 |
| A case study in formalizing projective geometry in Coq: Desargues theorem N Magaud, J Narboux, P Schreck Computational Geometry, 2012 | 25 | 2012 |
| Proof-checking Euclid M Beeson, J Narboux, F Wiedijk Annals of Mathematics and Artificial Intelligence 85, 213-257, 2019 | 21 | 2019 |
| Formalization of the arithmetization of Euclidean plane geometry and applications P Boutry, G Braun, J Narboux Journal of Symbolic Computation 90, 149-168, 2019 | 20 | 2019 |
| A synthetic proof of Pappus’ theorem in Tarski’s geometry G Braun, J Narboux Journal of Automated Reasoning 58, 209-230, 2017 | 19 | 2017 |
| Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq P Boutry, C Gries, J Narboux, P Schreck Journal of Automated Reasoning 62, 1-68, 2019 | 17* | 2019 |
| A vernacular for coherent logic S Stojanović, J Narboux, M Bezem, P Janičić Intelligent Computer Mathematics: International Conference, CICM 2014 …, 2014 | 17 | 2014 |
| A coq-based library for interactive and automated theorem proving in plane geometry TM Pham, Y Bertot, J Narboux Computational Science and Its Applications-ICCSA 2011, 368-383, 2011 | 16 | 2011 |
| A short note about case distinctions in Tarski's geometry P Boutry, J Narboux, P Schreck, G Braun Automated Deduction in Geometry 2014, 1-15, 2014 | 15 | 2014 |
Pascal Schreckprofesseur d'informatique, Université de StrasbourgVerified email at unistra.fr
