2019
- titre
- Proof-checking Euclid
- auteur
- Michael Beeson, Julien Narboux, Freek Wiedijk
- article
- Annals of Mathematics and Artificial Intelligence, Springer Verlag, 2019, pp.53. ⟨10.1007/s10472-018-9606-x⟩
- identifiant
- hal-01612807
- 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, Elsevier, 2019, Special Issue on Symbolic Computation in Software Science, 90, pp.149-168. ⟨10.1016/j.jsc.2018.04.007⟩
- identifiant
- hal-01483457
- Accès au texte intégral et bibtex
-
2018
- titre
- GeoCoq
- auteur
- Michael Beeson, Pierre Boutry, Gabriel Braun, Charly Gries, Julien Narboux
- article
- 2018, ⟨swh:1:dir:97ce53176b7d5e89d069bc60f49c3fa186831307⟩
- identifiant
- hal-01912024
- Accès au bibtex
-
2017
- 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, Springer Verlag, 2017, pp.68. ⟨10.1007/s10817-017-9422-8⟩
- identifiant
- hal-01178236
- Accès au texte intégral et bibtex
-
- titre
- A synthetic proof of Pappus' theorem in Tarski's geometry
- auteur
- Gabriel Braun, Julien Narboux
- article
- Journal of Automated Reasoning, Springer Verlag, 2017, 58 (2), pp.23. ⟨10.1007/s10817-016-9374-4⟩
- identifiant
- hal-01176508
- Accès au texte intégral et bibtex
-
2016
- 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
- identifiant
- hal-01282550
- 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
- identifiant
- hal-01332044
- 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
- identifiant
- hal-01228612
- Accès au texte intégral et bibtex
-
2015
- 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, Springer Verlag, 2015, 73 (3), pp.25. ⟨10.1007/s10472-014-9443-5⟩
- identifiant
- hal-01091011
- 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
- identifiant
- hal-01216750
- Accès au texte intégral et bibtex
-
2014
- 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
- identifiant
- hal-00989785
- 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
- identifiant
- hal-00989781
- Accès au texte intégral et bibtex
-
2012
- 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⟩
- identifiant
- hal-00727117
- Accès au texte intégral et bibtex
-
2006
- 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⟩
- identifiant
- inria-00118812
- Accès au texte intégral et bibtex
-