2024
Proceedings
- ref_biblio
- Julien Narboux, Walther Neuper, Pedro Quaresma. Proceedings 12th International Workshop on Theorem proving components for Educational software. 12th International Workshop on Theorem proving components for Educational software, Electronic Proceedings in Theoretical Computer Science, 400, EPTCS, 2024, Electronic Proceedings in Theoretical Computer Science, ⟨10.4204/eptcs.400⟩. ⟨hal-04537213⟩
- Accès au texte intégral et bibtex
-
2023
Journal articles
- ref_biblio
- Predrag Janičić, Julien Narboux. Automated generation of illustrated proofs in geometry and beyond. Annals of Mathematics and Artificial Intelligence, 2023, https://link.springer.com/article/10.1007/s10472-023-09857-y. ⟨10.1007/s10472-023-09857-y⟩. ⟨hal-04230795⟩
- Accès au texte intégral et bibtex
-
Conference papers
- ref_biblio
- Salwa Tabet Gonzalez, Predrag Janičić, Julien Narboux. Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving. Automated Deduction in Geometry 2023, Vesna Marinkovic; Danijela Simić; Sana Stojanović Đurđević; Milan Banković, Sep 2023, Belgrade, Serbia. ⟨hal-04226900⟩
- Accès au texte intégral et bibtex
-
- ref_biblio
- Julien Narboux. Formalisation, arithmetization and automatisation of geometry. Automated Deduction in Geometry 2023, Predrag Janičić; Pedro Quaresma; Zoltán Kovács; Vesna Marinković, Sep 2023, Belgrade, France. ⟨hal-04226945⟩
- Accès au bibtex
-
- ref_biblio
- Pierre Boutry, Julien Narboux. Tutorial Laboratory - GeoCoq to formalize high-school geometry problems. ADG 2023 - Automated Deduction in Geometry 2023, Predrag Janičić; Pedro Quaresma; Zoltán Kovács, Sep 2023, Belgrade, Serbia. ⟨hal-04230732⟩
- Accès au texte intégral et bibtex
-
- ref_biblio
- Evmorfia-Iro Bartzia, Emmanuel Beffara, Antoine Meyer, Julien Narboux. Underlying theories of proof assistants and potential impact on the teaching and learning of proof. 12th International Workshop on Theorem proving components for Educational software, Julien Narboux; Walther Neuper; Pedro Quaresma, Jul 2023, Rome, Italy. ⟨hal-04227823⟩
- Accès au bibtex
-
Preprints, Working Papers, ...
- ref_biblio
- Evmorfia-Iro Bartzia, Emmanuel Beffara, Antoine Meyer, Julien Narboux. Proof assistants for undergraduate mathematics education: elements of an a priori analysis. 2023. ⟨hal-04087080⟩
- Accès au texte intégral et bibtex
-
2022
Journal articles
- ref_biblio
- Predrag Janičić, Julien Narboux. Theorem Proving as Constraint Solving with Coherent Logic. Journal of Automated Reasoning, 2022, 66 (4), pp.689-746. ⟨10.1007/s10817-022-09629-z⟩. ⟨hal-03632665⟩
- Accès au texte intégral et bibtex
-
- ref_biblio
- Marie Kerjean, Frédéric Le Roux, Patrick Massot, Micaela Mayero, Zoé Mesnil, et al.. Utilisation des assistants de preuves pour l’enseignement en L1 : Retours d’expériences. La gazette des mathématiciens, 2022, 174. ⟨hal-03979238⟩
- Accès au texte intégral et bibtex
-
Conference papers
- ref_biblio
- Evmorfia Bartzia, Antoine Meyer, Julien Narboux. Proof assistants for undergraduate mathematics and computer science education: elements of a priori analysis. INDRUM 2022: Fourth conference of the International Network for Didactic Research in University Mathematics, Reinhard Hochmuth, Oct 2022, Hanovre, Germany. ⟨hal-03648357v2⟩
- Accès au texte intégral et bibtex
-
Book sections
- ref_biblio
- Julien Narboux, Viviane Durand-Guerrier. Combining pencil/paper proofs and formal proofs, a challenge for Artificial Intelligence and mathematics education. Richard P.R.; Vélez M.P.; Van Vaerenbergh S. Mathematics Education in the Age of Artificial Intelligence: How Intelligence can serve mathematical human learning, 17, Springer, pp.167-192, 2022, Mathematics Education in the Digital Era, 978-3-030-86908-3. ⟨10.1007/978-3-030-86909-0_8⟩. ⟨hal-03254579⟩
- Accès au texte intégral et bibtex
-
2021
Journal articles
- ref_biblio
- Basile Sauvage, Jean-Christophe Grimont, Régine Hamm-Audonnet, Julien Narboux. Découvrir des concepts informatiques autour des arbres binaires, Une série d’activités d’informatique débranchée. Repères, 2021, 125. ⟨hal-03797893⟩
- Accès au bibtex
-
- ref_biblio
- Julien Narboux, Cristel Pelsser, Basile Sauvage, Gaelle Thomas. La cordée de la réussite "décodeuses d'informatique". 1024 : Bulletin de la Société Informatique de France, 2021, 18, pp.87-89. ⟨10.48556/SIF.1024.18.87⟩. ⟨hal-04476335⟩
- Accès au texte intégral et bibtex
-
Conference papers
- ref_biblio
- Predrag Janičić, Julien Narboux. Automated Generation of Illustrations for Synthetic Geometry Proofs. Automated Deduction in Geometry, Zoltán Kovács, Sep 2021, Hagenberg, Austria. pp.91-102, ⟨10.4204/EPTCS.352.9⟩. ⟨hal-03327987⟩
- Accès au texte intégral et bibtex
-
- ref_biblio
- Salwa Tabet Gonzalez, Stéphane Graham-Lengrand, Julien Narboux, Natarajan Shankar. Semantic parsing of geometry statements using supervised machine learning on synthetic data. NatFoM 2021 - CICM Workshop, Peter Koepke, Bonn; Dennis Müller, Erlangen, Jul 2021, Timisoara, Romania. ⟨hal-03327994⟩
- Accès au texte intégral et bibtex
-
2019
Journal articles
- ref_biblio
- Pierre Boutry, Gabriel Braun, Julien Narboux. Formalization of the Arithmetization of Euclidean Plane Geometry and Applications. Journal of Symbolic Computation, 2019, Special Issue on Symbolic Computation in Software Science, 90, pp.149-168. ⟨10.1016/j.jsc.2018.04.007⟩. ⟨hal-01483457⟩
- Accès au texte intégral et bibtex
-
- ref_biblio
- Pierre Boutry, Charly Gries, Julien Narboux, Pascal Schreck. Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq. Journal of Automated Reasoning, 2019, 62 (1), pp.68. ⟨10.1007/s10817-017-9422-8⟩. ⟨hal-01178236v2⟩
- Accès au texte intégral et bibtex
-
- ref_biblio
- Michael Beeson, Julien Narboux, Freek Wiedijk. Proof-checking Euclid. Annals of Mathematics and Artificial Intelligence, 2019, pp.53. ⟨10.1007/s10472-018-9606-x⟩. ⟨hal-01612807v3⟩
- Accès au texte intégral et bibtex
-
Conference papers
- ref_biblio
- Charly Gries, Julien Narboux, Pierre Boutry. Axiomes de continuité en géométrie neutre : une étude mécanisée en Coq. Journées Francophones des Langages Applicatifs 2019, Jan 2019, Les Rousses, France. ⟨hal-01923814v2⟩
- Accès au texte intégral et bibtex
-
2018
Book sections
- ref_biblio
- Julien Narboux, Predrag Janicic, Jacques Fleuriot. Computer-assisted Theorem Proving in Synthetic Geometry. Meera Sitharam; Audrey St. John; Jessica Sidman. Handbook of Geometric Constraint Systems Principles, Chapman and Hall/CRC , In press, Discrete Mathematics and Its Applications, 1498738915. ⟨hal-01779452⟩
- Accès au bibtex
-
Software
- ref_biblio
- Michael Beeson, Pierre Boutry, Gabriel Braun, Charly Gries, Julien Narboux. GeoCoq. 2018, ⟨swh:1:dir:97ce53176b7d5e89d069bc60f49c3fa186831307;origin=https://hal.archives-ouvertes.fr/hal-01912024;visit=swh:1:snp:1cbf6e8cee9dde43b03c16566f00122653381227;anchor=swh:1:rev:640e8d6a4813be6b44bee473dfb674f40daac1f0;path=/⟩. ⟨hal-01912024⟩
- Accès au texte intégral et bibtex
-
2017
Journal articles
- ref_biblio
- Gabriel Braun, Julien Narboux. A synthetic proof of Pappus' theorem in Tarski's geometry. Journal of Automated Reasoning, 2017, 58 (2), pp.23. ⟨10.1007/s10817-016-9374-4⟩. ⟨hal-01176508v2⟩
- Accès au texte intégral et bibtex
-
2016
Journal articles
- ref_biblio
- Julien Narboux, David Braun. Towards A Certified Version of the Encyclopedia of Triangle Centers. Mathematics in Computer Science, 2016, 10 (1), pp.17. ⟨10.1007/s11786-016-0254-4⟩. ⟨hal-01174131v2⟩
- Accès au texte intégral et bibtex
-
Conference papers
- ref_biblio
- Gabriel Braun, Pierre Boutry, Julien Narboux. From Hilbert to Tarski. Eleventh International Workshop on Automated Deduction in Geometry, Jun 2016, Strasbourg, France. pp.19. ⟨hal-01332044⟩
- Accès au texte intégral et bibtex
-
- ref_biblio
- Pierre Boutry, Gabriel Braun, Julien Narboux. From Tarski to Descartes: Formalization of the Arithmetization of Euclidean Geometry. SCSS 2016, the 7th International Symposium on Symbolic Computation in Software Science, Mar 2016, Tokyo, Japan. pp.14-28. ⟨hal-01282550⟩
- Accès au texte intégral et bibtex
-
- ref_biblio
- Charly Gries, Pierre Boutry, Julien Narboux. Somme des angles d'un triangle et unicité de la parallèle : une preuve d'équivalence formalisée en Coq. Les vingt-septièmes Journées Francophones des Langages Applicatifs (JFLA 2016), Jade Algave; Julien Signoles, Jan 2016, Saint Malo, France. pp.15. ⟨hal-01228612v2⟩
- Accès au texte intégral et bibtex
-
Books
- ref_biblio
- Julien Narboux, Pascal Schreck, Ileana Streinu (Dir.). Proceedings of ADG 2016: Eleventh International Workshop on Automated Deduction in Geometry. , pp.224, 2016. ⟨hal-01334334⟩
- Accès au texte intégral et bibtex
-
2015
Journal articles
- ref_biblio
- Sana Stojanovic Durdevic, Julien Narboux, Predrag Janicic. Automated Generation of Machine Verifiable and Readable Proofs: A Case Study of Tarski's Geometry. Annals of Mathematics and Artificial Intelligence, 2015, 73 (3), pp.25. ⟨10.1007/s10472-014-9443-5⟩. ⟨hal-01091011v2⟩
- Accès au texte intégral et bibtex
-
- ref_biblio
- Michael Beeson, Pierre Boutry, Julien Narboux. Herbrand's theorem and non-Euclidean geometry. Bulletin of Symbolic Logic, 2015, 21 (2), pp.12. ⟨10.1017/bsl.2015.6⟩. ⟨hal-01071431v3⟩
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- ref_biblio
- Pierre Boutry, Julien Narboux, Pascal Schreck. A reflexive tactic for automated generation of proofs of incidence to an affine variety. 2015. ⟨hal-01216750⟩
- Accès au texte intégral et bibtex
-
2014
Conference papers
- ref_biblio
- Pierre Boutry, Julien Narboux, Pascal Schreck, Gabriel Braun. A short note about case distinctions in Tarski's geometry. Automated Deduction in Geometry 2014, Jul 2014, Coimbra, Portugal. pp.1-15. ⟨hal-00989785v2⟩
- Accès au texte intégral et bibtex
-
- ref_biblio
- Sana Stojanovic, Julien Narboux, Marc Bezem, Predrag Janicic. A Vernacular for Coherent Logic. CICM 2014 - Conferences on Intelligent Computer Mathematics, Jul 2014, Coimbra, Portugal. pp.16, ⟨10.1007/978-3-319-08434-3_28⟩. ⟨hal-00983975v2⟩
- Accès au texte intégral et bibtex
-
- ref_biblio
- Pierre Boutry, Julien Narboux, Pascal Schreck, Gabriel Braun. Using small scale automation to improve both accessibility and readability of formal proofs in geometry. Automated Deduction in Geometry 2014, Jul 2014, Coimbra, Portugal. pp.1-19. ⟨hal-00989781v2⟩
- Accès au texte intégral et bibtex
-
2013
Documents associated with scientific events
- ref_biblio
- Julien Narboux. Les assistants de preuve, ou comment avoir confiance en ses démonstrations.. Séminaire L, Mar 2013, Strasbourg, France. ⟨hal-00809448⟩
- Accès au texte intégral et bibtex
-
2012
Journal articles
- ref_biblio
- Nicolas Magaud, Julien Narboux, Pascal Schreck. A Case Study in Formalizing Projective Geometry in Coq: Desargues Theorem. Computational Geometry, 2012, Special Issue on geometric reasoning, 45 (8), pp.406-424. ⟨10.1016/j.comgeo.2010.06.004⟩. ⟨inria-00432810v2⟩
- Accès au texte intégral et bibtex
-
- ref_biblio
- Predrag Janicic, Julien Narboux, Pedro Quaresma. The Area Method : a Recapitulation. Journal of Automated Reasoning, 2012, 48 (4), pp.489-532. ⟨10.1007/s10817-010-9209-7⟩. ⟨hal-00426563v2⟩
- Accès au texte intégral et bibtex
-
Conference papers
- ref_biblio
- Bruno Cuervo Parrino, Julien Narboux, Eric Violard, Nicolas Magaud. Dealing with arithmetic overflows in the polyhedral model. IMPACT 2012 - 2nd International Workshop on Polyhedral Compilation Techniques, Louis-Noel Pouchet, Jan 2012, Paris, France. ⟨hal-00655485⟩
- Accès au texte intégral et bibtex
-
- ref_biblio
- Gabriel Braun, Julien Narboux. From Tarski to Hilbert. Automated Deduction in Geometry 2012, Jacques Fleuriot, Sep 2012, Edinburgh, United Kingdom. pp.89-109, ⟨10.1007/978-3-642-40672-0_7⟩. ⟨hal-00727117v2⟩
- Accès au texte intégral et bibtex
-
- ref_biblio
- Pascal Schreck, Pascal Mathis, Julien Narboux. Geometric Construction Problem Solving in Computer-Aided Learning. 24th IEEE International Conference on Tools with Artificial Intelligence, Nov 2012, Athens, Greece. pp.1139 - 1144, ⟨10.1109/ICTAI.2012.162⟩. ⟨hal-00753551⟩
- Accès au texte intégral et bibtex
-
2011
Conference papers
- ref_biblio
- Tuan Minh Pham, Yves Bertot, Julien Narboux. A Coq-based Library for Interactive and Automated Theorem Proving in Plane Geometry. The 11th International Conference on Computational Science and Its Applications (ICCSA 2011), Jun 2011, Santander, Spain. pp.368-383, ⟨10.1007/978-3-642-21898-9_32⟩. ⟨inria-00584918⟩
- Accès au texte intégral et bibtex
-
- ref_biblio
- Jean-David Génevaux, Julien Narboux, Pascal Schreck. Formalization of Wu's simple method in Coq. CPP 2011 First International Conference on Certified Programs and Proofs, Dec 2011, Kenting, Taiwan. pp.71-86, ⟨10.1007/978-3-642-25379-9_8⟩. ⟨inria-00618745v2⟩
- Accès au texte intégral et bibtex
-
Books
- ref_biblio
- Julien Narboux, Schreck Pascal, Jürgen Richter-Gebert (Dir.). Automated Deduction in Geometry - 8th International Workshop, Revised Selected Papers. Pascal Schreck and Julien Narboux and Jürgen Richter-Gebert. Springer, 6877, pp.258, 2011, Lecture Notes in Computer Science, 978-3-642-25069-9. ⟨10.1007/978-3-642-25070-5⟩. ⟨hal-00644313⟩
- Accès au bibtex
-
2009
Conference papers
- ref_biblio
- Nicolas Magaud, Julien Narboux, Pascal Schreck. Formalizing Desargues' theorem in Coq using ranks in Coq. 24th Annual ACM Symposium on Applied Computing, Xiao-Shan Gao, Robert Joan-Arinyo, Dominique Michelucci, Mar 2009, Honolulu, United States. pp.1110-1115, ⟨10.1145/1529282.1529527⟩. ⟨inria-00335719⟩
- Accès au texte intégral et bibtex
-
2008
Conference papers
- ref_biblio
- Christian Urban, Julien Narboux. Formal SOS-Proofs for the Lambda-Calculus. Third Workshop on Logical and Semantic Frameworks, with Applications, Mauricio Ayala-Rincón, Aug 2008, Salvador, Brazil. pp.139-155, ⟨10.1016/j.entcs.2009.07.053⟩. ⟨inria-00335718⟩
- Accès au texte intégral et bibtex
-
- ref_biblio
- Nicolas Magaud, Julien Narboux, Pascal Schreck. Formalizing Projective Plane Geometry in Coq. Post-proceedings of Automated Deduction in Geometry (ADG) 2008, Thomas Sturm, Sep 2008, Shanghai, China. pp.141-162, ⟨10.1007/978-3-642-21046-4⟩. ⟨inria-00305998v3⟩
- Accès au texte intégral et bibtex
-
2007
Journal articles
- ref_biblio
- Julien Narboux. A Graphical User Interface for Formal Proofs in Geometry.. Journal of Automated Reasoning, 2007, Special Issue on User Interfaces in Theorem Proving, 39 (2), pp.161-180. ⟨10.1007/s10817-007-9071-4⟩. ⟨inria-00118903⟩
- Accès au texte intégral et bibtex
-
Conference papers
- ref_biblio
- Julien Narboux, Christian Urban. Formalising in Nominal Isabelle Crary's Completeness Proof for Equivalence Checking.. LFMTP'07, Jul 2007, Bremen, Germany. 15p., ⟨10.1016/j.entcs.2007.09.014⟩. ⟨inria-00180061v2⟩
- Accès au texte intégral et bibtex
-
- ref_biblio
- Julien Narboux. GeoProof: A user interface for formal proofs in geometry. MathUI 07, Jun 2007, Linz, Austria. ⟨inria-00495958⟩
- Accès au bibtex
-
2006
Conference papers
- ref_biblio
- Julien Narboux. Mechanical Theorem Proving in Tarski's geometry.. Automated Deduction in Geometry 2006, Francisco Botana, Aug 2006, Pontevedra, Spain. pp.139-156, ⟨10.1007/978-3-540-77356-6⟩. ⟨inria-00118812⟩
- Accès au texte intégral et bibtex
-
Theses
- ref_biblio
- Julien Narboux. Formalisation et automatisation du raisonnement géométrique en Coq.. Autre [cs.OH]. Université Paris Sud - Paris XI, 2006. Français. ⟨NNT : ⟩. ⟨tel-00118806⟩
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- ref_biblio
- Julien Narboux. A formalization of diagrammatic proofs in abstract rewriting. 2006. ⟨inria-00180065⟩
- Accès au texte intégral et bibtex
-
2005
Conference papers
- ref_biblio
- Julien Narboux. Toward the use of a proof assistant to teach mathematics. The Seventh International Conference on Technology in Mathematics Teaching (ICTMT7), Jul 2005, Bristol, United Kingdom. ⟨inria-00495952⟩
- Accès au texte intégral et bibtex
-
2004
Conference papers
- ref_biblio
- Julien Narboux. A Decision Procedure for Geometry in Coq. Theorem Proving in Higher Order Logics 2004, Jul 2004, Park City, USA, United States. pp.225-240, ⟨10.1007/b100400⟩. ⟨inria-00001035⟩
- Accès au texte intégral et bibtex
-