Publications HAL de la collection GeoCoq

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
https://hal.archives-ouvertes.fr/hal-01612807/file/ProofCheckingEuclid.pdf 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
https://hal.inria.fr/hal-01483457/file/extended-arithmetization.pdf 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
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
https://hal.inria.fr/hal-01178236/file/parallel_postulates_revised.pdf 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
https://hal.inria.fr/hal-01176508/file/Pappus.pdf 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
https://hal.archives-ouvertes.fr/hal-01282550/file/arithmetization.pdf 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
https://hal.inria.fr/hal-01332044/file/hilbert_to_tarski.pdf 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
https://hal.inria.fr/hal-01228612/file/jfla2016-gries-boutry-narboux.pdf 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
https://hal.inria.fr/hal-01091011/file/AFTarski.pdf 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
https://hal.inria.fr/hal-01216750/file/main.pdf 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
https://hal.inria.fr/hal-00989785/file/Tarski_case_distinction_proceedings.pdf 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
https://hal.inria.fr/hal-00989781/file/small-scale-automation-Tarski-proceedings.pdf 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
https://hal.inria.fr/hal-00727117/file/adg2012_braun_narboux_postproc.pdf 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
https://hal.inria.fr/inria-00118812/file/adg06-narboux.pdf BibTex