Journal articles
- titre
- A synthetic proof of Pappus' theorem in Tarski's geometry
- auteur
- Gabriel Braun, Julien Narboux
- article
- Journal of Automated Reasoning, 2017, 58 (2), pp.23. ⟨10.1007/s10817-016-9374-4⟩
- Accès au texte intégral et bibtex
-
- titre
- La cordée de la réussite "décodeuses d'informatique
- auteur
- Julien Narboux, Cristel Pelsser, Basile Sauvage, Gaelle Thomas
- article
- 1024 : Bulletin de la Société Informatique de France, 2021, 18, pp.87-89. ⟨10.48556/SIF.1024.18.87⟩
- Accès au texte intégral et bibtex
-
- titre
- Découvrir des concepts informatiques autour des arbres binaires, Une série d’activités d’informatique débranchée
- auteur
- Basile Sauvage, Jean-Christophe Grimont, Régine Hamm-Audonnet, Julien Narboux
- article
- Repères, 2021, 125
- Accès au bibtex
-
- titre
- Automated Generation of Machine Verifiable and Readable Proofs: A Case Study of Tarski's Geometry
- auteur
- Sana Stojanovic Durdevic, Julien Narboux, Predrag Janicic
- article
- Annals of Mathematics and Artificial Intelligence, 2015, 73 (3), pp.25. ⟨10.1007/s10472-014-9443-5⟩
- Accès au texte intégral et bibtex
-
- titre
- Theorem Proving as Constraint Solving with Coherent Logic
- auteur
- Predrag Janičić, Julien Narboux
- article
- Journal of Automated Reasoning, 2022, 66 (4), pp.689-746. ⟨10.1007/s10817-022-09629-z⟩
- Accès au texte intégral et bibtex
-
- titre
- A Case Study in Formalizing Projective Geometry in Coq: Desargues Theorem
- auteur
- Nicolas Magaud, Julien Narboux, Pascal Schreck
- article
- Computational Geometry, 2012, Special Issue on geometric reasoning, 45 (8), pp.406-424. ⟨10.1016/j.comgeo.2010.06.004⟩
- Accès au texte intégral et bibtex
-
- titre
- The Area Method : a Recapitulation
- auteur
- Predrag Janicic, Julien Narboux, Pedro Quaresma
- article
- Journal of Automated Reasoning, 2012, 48 (4), pp.489-532. ⟨10.1007/s10817-010-9209-7⟩
- Accès au texte intégral et bibtex
-
- titre
- A Graphical User Interface for Formal Proofs in Geometry.
- auteur
- Julien Narboux
- article
- Journal of Automated Reasoning, 2007, Special Issue on User Interfaces in Theorem Proving, 39 (2), pp.161-180. ⟨10.1007/s10817-007-9071-4⟩
- Accès au texte intégral et bibtex
-
- titre
- Proof-checking Euclid
- auteur
- Michael Beeson, Julien Narboux, Freek Wiedijk
- article
- Annals of Mathematics and Artificial Intelligence, 2019, pp.53. ⟨10.1007/s10472-018-9606-x⟩
- Accès au texte intégral et bibtex
-
- titre
- Automated generation of illustrated proofs in geometry and beyond
- auteur
- Predrag Janičić, Julien Narboux
- article
- Annals of Mathematics and Artificial Intelligence, 2023, https://link.springer.com/article/10.1007/s10472-023-09857-y. ⟨10.1007/s10472-023-09857-y⟩
- Accès au texte intégral et bibtex
-
- titre
- Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
- auteur
- Pierre Boutry, Charly Gries, Julien Narboux, Pascal Schreck
- article
- Journal of Automated Reasoning, 2019, 62 (1), pp.68. ⟨10.1007/s10817-017-9422-8⟩
- Accès au texte intégral et bibtex
-
- titre
- Utilisation des assistants de preuves pour l’enseignement en L1
- auteur
- Marie Kerjean, Frédéric Le Roux, Patrick Massot, Micaela Mayero, Zoé Mesnil, Simon Modeste, Julien Narboux, Pierre Rousselin
- article
- La gazette des mathématiciens, 2022, 174
- Accès au texte intégral et bibtex
-
- titre
- Towards A Certified Version of the Encyclopedia of Triangle Centers
- auteur
- Julien Narboux, David Braun
- article
- Mathematics in Computer Science, 2016, 10 (1), pp.17. ⟨10.1007/s11786-016-0254-4⟩
- Accès au texte intégral et bibtex
-
- titre
- Herbrand's theorem and non-Euclidean geometry
- auteur
- Michael Beeson, Pierre Boutry, Julien Narboux
- article
- Bulletin of Symbolic Logic, 2015, 21 (2), pp.12. ⟨10.1017/bsl.2015.6⟩
- Accès au texte intégral et bibtex
-
- titre
- Formalization of the Arithmetization of Euclidean Plane Geometry and Applications
- auteur
- Pierre Boutry, Gabriel Braun, Julien Narboux
- article
- Journal of Symbolic Computation, 2019, Special Issue on Symbolic Computation in Software Science, 90, pp.149-168. ⟨10.1016/j.jsc.2018.04.007⟩
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Geometric Construction Problem Solving in Computer-Aided Learning
- auteur
- Pascal Schreck, Pascal Mathis, Julien Narboux
- article
- 24th IEEE International Conference on Tools with Artificial Intelligence, Nov 2012, Athens, Greece. pp.1139 - 1144, ⟨10.1109/ICTAI.2012.162⟩
- Accès au texte intégral et bibtex
-
- titre
- Formalisation, arithmetization and automatisation of geometry
- auteur
- Julien Narboux
- article
- Automated Deduction in Geometry 2023, Predrag Janičić; Pedro Quaresma; Zoltán Kovács; Vesna Marinković, Sep 2023, Belgrade, France
- Accès au bibtex
-
- titre
- From Tarski to Hilbert
- auteur
- Gabriel Braun, Julien Narboux
- article
- Automated Deduction in Geometry 2012, Jacques Fleuriot, Sep 2012, Edinburgh, United Kingdom. pp.89-109, ⟨10.1007/978-3-642-40672-0_7⟩
- Accès au texte intégral et bibtex
-
- titre
- A Vernacular for Coherent Logic
- auteur
- Sana Stojanovic, Julien Narboux, Marc Bezem, Predrag Janicic
- article
- CICM 2014 - Conferences on Intelligent Computer Mathematics, Jul 2014, Coimbra, Portugal. pp.16, ⟨10.1007/978-3-319-08434-3_28⟩
- Accès au texte intégral et bibtex
-
- titre
- Underlying theories of proof assistants and potential impact on the teaching and learning of proof
- auteur
- Evmorfia-Iro Bartzia, Emmanuel Beffara, Antoine Meyer, Julien Narboux
- article
- 12th International Workshop on Theorem proving components for Educational software, Julien Narboux; Walther Neuper; Pedro Quaresma, Jul 2023, Rome, Italy
- Accès au bibtex
-
- titre
- Formalizing Desargues' theorem in Coq using ranks in Coq
- auteur
- Nicolas Magaud, Julien Narboux, Pascal Schreck
- article
- 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⟩
- Accès au texte intégral et bibtex
-
- titre
- Somme des angles d'un triangle et unicité de la parallèle : une preuve d'équivalence formalisée en Coq
- auteur
- Charly Gries, Pierre Boutry, Julien Narboux
- article
- Les vingt-septièmes Journées Francophones des Langages Applicatifs (JFLA 2016), Jade Algave; Julien Signoles, Jan 2016, Saint Malo, France. pp.15
- Accès au texte intégral et bibtex
-
- titre
- Axiomes de continuité en géométrie neutre : une étude mécanisée en Coq
- auteur
- Charly Gries, Julien Narboux, Pierre Boutry
- article
- Journées Francophones des Langages Applicatifs 2019, Jan 2019, Les Rousses, France
- Accès au texte intégral et bibtex
-
- titre
- Mechanical Theorem Proving in Tarski's geometry.
- auteur
- Julien Narboux
- article
- Automated Deduction in Geometry 2006, Francisco Botana, Aug 2006, Pontevedra, Spain. pp.139-156, ⟨10.1007/978-3-540-77356-6⟩
- Accès au texte intégral et bibtex
-
- titre
- A Decision Procedure for Geometry in Coq
- auteur
- Julien Narboux
- article
- Theorem Proving in Higher Order Logics 2004, Jul 2004, Park City, USA, United States. pp.225-240, ⟨10.1007/b100400⟩
- Accès au texte intégral et bibtex
-
- titre
- GeoProof: A user interface for formal proofs in geometry
- auteur
- Julien Narboux
- article
- MathUI 07, Jun 2007, Linz, Austria
- Accès au bibtex
-
- titre
- A Coq-based Library for Interactive and Automated Theorem Proving in Plane Geometry
- auteur
- Tuan Minh Pham, Yves Bertot, Julien Narboux
- article
- 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⟩
- Accès au texte intégral et bibtex
-
- titre
- Formalizing Projective Plane Geometry in Coq
- auteur
- Nicolas Magaud, Julien Narboux, Pascal Schreck
- article
- 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⟩
- Accès au texte intégral et bibtex
-
- titre
- Semantic parsing of geometry statements using supervised machine learning on synthetic data
- auteur
- Salwa Tabet Gonzalez, Stéphane Graham-Lengrand, Julien Narboux, Natarajan Shankar
- article
- NatFoM 2021 - CICM Workshop, Peter Koepke, Bonn; Dennis Müller, Erlangen, Jul 2021, Timisoara, Romania
- Accès au texte intégral et bibtex
-
- titre
- Tutorial Laboratory - GeoCoq to formalize high-school geometry problems
- auteur
- Pierre Boutry, Julien Narboux
- article
- ADG 2023 - Automated Deduction in Geometry 2023, Predrag Janičić; Pedro Quaresma; Zoltán Kovács, Sep 2023, Belgrade, Serbia
- Accès au texte intégral et bibtex
-
- titre
- Automated Generation of Illustrations for Synthetic Geometry Proofs
- auteur
- Predrag Janičić, Julien Narboux
- article
- Automated Deduction in Geometry, Zoltán Kovács, Sep 2021, Hagenberg, Austria. pp.91-102, ⟨10.4204/EPTCS.352.9⟩
- Accès au texte intégral et bibtex
-
- titre
- Using small scale automation to improve both accessibility and readability of formal proofs in geometry
- auteur
- Pierre Boutry, Julien Narboux, Pascal Schreck, Gabriel Braun
- article
- Automated Deduction in Geometry 2014, Jul 2014, Coimbra, Portugal. pp.1-19
- Accès au texte intégral et bibtex
-
- titre
- From Tarski to Descartes: Formalization of the Arithmetization of Euclidean Geometry
- auteur
- Pierre Boutry, Gabriel Braun, Julien Narboux
- article
- SCSS 2016, the 7th International Symposium on Symbolic Computation in Software Science, Mar 2016, Tokyo, Japan. pp.14-28
- Accès au texte intégral et bibtex
-
- titre
- Formalising in Nominal Isabelle Crary's Completeness Proof for Equivalence Checking.
- auteur
- Julien Narboux, Christian Urban
- article
- LFMTP'07, Jul 2007, Bremen, Germany. 15p., ⟨10.1016/j.entcs.2007.09.014⟩
- Accès au texte intégral et bibtex
-
- titre
- Toward the use of a proof assistant to teach mathematics
- auteur
- Julien Narboux
- article
- The Seventh International Conference on Technology in Mathematics Teaching (ICTMT7), Jul 2005, Bristol, United Kingdom
- Accès au texte intégral et bibtex
-
- titre
- Formal SOS-Proofs for the Lambda-Calculus
- auteur
- Christian Urban, Julien Narboux
- article
- 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⟩
- Accès au texte intégral et bibtex
-
- titre
- Dealing with arithmetic overflows in the polyhedral model
- auteur
- Bruno Cuervo Parrino, Julien Narboux, Eric Violard, Nicolas Magaud
- article
- IMPACT 2012 - 2nd International Workshop on Polyhedral Compilation Techniques, Louis-Noel Pouchet, Jan 2012, Paris, France
- Accès au texte intégral et bibtex
-
- titre
- From Hilbert to Tarski
- auteur
- Gabriel Braun, Pierre Boutry, Julien Narboux
- article
- Eleventh International Workshop on Automated Deduction in Geometry, Jun 2016, Strasbourg, France. pp.19
- Accès au texte intégral et bibtex
-
- titre
- Formalization of Wu's simple method in Coq
- auteur
- Jean-David Génevaux, Julien Narboux, Pascal Schreck
- article
- 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⟩
- Accès au texte intégral et bibtex
-
- titre
- Proof assistants for undergraduate mathematics and computer science education: elements of a priori analysis
- auteur
- Evmorfia Bartzia, Antoine Meyer, Julien Narboux
- article
- INDRUM 2022: Fourth conference of the International Network for Didactic Research in University Mathematics, Reinhard Hochmuth, Oct 2022, Hanovre, Germany
- Accès au texte intégral et bibtex
-
- titre
- A short note about case distinctions in Tarski's geometry
- auteur
- Pierre Boutry, Julien Narboux, Pascal Schreck, Gabriel Braun
- article
- Automated Deduction in Geometry 2014, Jul 2014, Coimbra, Portugal. pp.1-15
- Accès au texte intégral et bibtex
-
- titre
- Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving
- auteur
- Salwa Tabet Gonzalez, Predrag Janičić, Julien Narboux
- article
- Automated Deduction in Geometry 2023, Vesna Marinkovic; Danijela Simić; Sana Stojanović Đurđević; Milan Banković, Sep 2023, Belgrade, Serbia
- Accès au texte intégral et bibtex
-
Book sections
- titre
- Computer-assisted Theorem Proving in Synthetic Geometry
- auteur
- Julien Narboux, Predrag Janicic, Jacques Fleuriot
- article
- 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
- Accès au bibtex
-
- titre
- Combining pencil/paper proofs and formal proofs, a challenge for Artificial Intelligence and mathematics education
- auteur
- Julien Narboux, Viviane Durand-Guerrier
- article
- 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⟩
- Accès au texte intégral et bibtex
-
Books
- titre
- Automated Deduction in Geometry - 8th International Workshop, Revised Selected Papers
- auteur
- Julien Narboux, Schreck Pascal, Jürgen Richter-Gebert
- article
- 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⟩
- Accès au bibtex
-
- titre
- Proceedings of ADG 2016
- auteur
- Julien Narboux, Pascal Schreck, Ileana Streinu
- article
- , pp.224, 2016
- Accès au texte intégral et bibtex
-
Documents associated with scientific events
- titre
- Les assistants de preuve, ou comment avoir confiance en ses démonstrations.
- auteur
- Julien Narboux
- article
- Séminaire L, Mar 2013, Strasbourg, France
- Accès au texte intégral et bibtex
-
Proceedings
- titre
- Proceedings 12th International Workshop on Theorem proving components for Educational software
- auteur
- Julien Narboux, Walther Neuper, Pedro Quaresma
- article
- 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⟩
- Accès au texte intégral et bibtex
-
Software
- titre
- GeoCoq
- auteur
- Michael Beeson, Pierre Boutry, Gabriel Braun, Charly Gries, Julien Narboux
- article
- 2018, ⟨swh:1:dir:97ce53176b7d5e89d069bc60f49c3fa186831307;origin=https://hal.archives-ouvertes.fr/hal-01912024;visit=swh:1:snp:1cbf6e8cee9dde43b03c16566f00122653381227;anchor=swh:1:rev:640e8d6a4813be6b44bee473dfb674f40daac1f0;path=/⟩
- Accès au texte intégral et bibtex
-
Theses
- titre
- Formalisation et automatisation du raisonnement géométrique en Coq.
- auteur
- Julien Narboux
- article
- Autre [cs.OH]. Université Paris Sud - Paris XI, 2006. Français. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
- titre
- A formalization of diagrammatic proofs in abstract rewriting
- auteur
- Julien Narboux
- article
- 2006
- Accès au texte intégral et bibtex
-
- titre
- A reflexive tactic for automated generation of proofs of incidence to an affine variety
- auteur
- Pierre Boutry, Julien Narboux, Pascal Schreck
- article
- 2015
- Accès au texte intégral et bibtex
-
- titre
- Proof assistants for undergraduate mathematics education: elements of an a priori analysis
- auteur
- Evmorfia-Iro Bartzia, Emmanuel Beffara, Antoine Meyer, Julien Narboux
- article
- 2023
- Accès au texte intégral et bibtex
-