Filtrer vos résultats
- 16
- 8
- 4
- 2
- 1
- 1
- 1
- 16
- 1
- 2
- 1
- 3
- 2
- 3
- 2
- 2
- 13
- 2
- 1
- 14
- 4
- 1
- 1
- 16
- 12
- 3
- 3
- 3
- 3
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
16 résultats
|
|
|
triés par
|
|
|
Axiomes de continuité en géométrie neutre : une étude mécanisée en CoqJournées Francophones des Langages Applicatifs 2019, Jan 2019, Les Rousses, France
Communication dans un congrès
hal-01923814v2
|
||
|
|
CV2EC: Getting the Best of Both Worlds2023
Pré-publication, Document de travail
hal-04321656v1
|
||
|
|
On the Formalization of Foundations of GeometryLogic in Computer Science [cs.LO]. Université de Strasbourg, 2018. English. ⟨NNT : ⟩
Thèse
tel-02012674v1
|
||
|
|
Formalization of the Arithmetization of Euclidean Plane Geometry and ApplicationsJournal of Symbolic Computation, 2019, Special Issue on Symbolic Computation in Software Science, 90, pp.149-168. ⟨10.1016/j.jsc.2018.04.007⟩
Article dans une revue
hal-01483457v1
|
||
|
|
Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using CoqJournal of Automated Reasoning, 2019, 62 (1), pp.68. ⟨10.1007/s10817-017-9422-8⟩
Article dans une revue
hal-01178236v2
|
||
|
|
From Hilbert to TarskiEleventh International Workshop on Automated Deduction in Geometry, Jun 2016, Strasbourg, France. pp.19
Communication dans un congrès
hal-01332044v1
|
||
|
|
A reflexive tactic for automated generation of proofs of incidence to an affine variety2015
Pré-publication, Document de travail
hal-01216750v1
|
||
|
|
A short note about case distinctions in Tarski's geometryAutomated Deduction in Geometry 2014, Jul 2014, Coimbra, Portugal. pp.1-15
Communication dans un congrès
hal-00989785v2
|
||
|
|
Herbrand's theorem and non-Euclidean geometryBulletin of Symbolic Logic, 2015, 21 (2), pp.12. ⟨10.1017/bsl.2015.6⟩
Article dans une revue
hal-01071431v3
|
||
|
|
Using small scale automation to improve both accessibility and readability of formal proofs in geometryAutomated Deduction in Geometry 2014, Jul 2014, Coimbra, Portugal. pp.1-19
Communication dans un congrès
hal-00989781v2
|
||
|
|
Formalization of the Poincaré Disc Model of Hyperbolic GeometryJournal of Automated Reasoning, 2020, 65 (1), pp.31-73. ⟨10.1007/s10817-020-09551-2⟩
Article dans une revue
hal-03120829v1
|
||
|
|
From Tarski to Descartes: Formalization of the Arithmetization of Euclidean GeometrySCSS 2016, the 7th International Symposium on Symbolic Computation in Software Science, Mar 2016, Tokyo, Japan. pp.14-28
Communication dans un congrès
hal-01282550v1
|
||
|
|
Tutorial Laboratory - GeoCoq to formalize high-school geometry problemsADG 2023 - Automated Deduction in Geometry 2023, Predrag Janičić; Pedro Quaresma; Zoltán Kovács, Sep 2023, Belgrade, Serbia
Communication dans un congrès
hal-04230732v1
|
||
|
|
Towards an Independent Version of Tarski's System of Geometry14th International Conference on Automated Deduction in Geometry, Sep 2023, Belgrade, Serbia. pp.73-84, ⟨10.4204/EPTCS.398.11⟩
Communication dans un congrès
hal-04324071v1
|
||
|
|
GeoCoqLogiciel hal-01912024v1 |
||
|
|
Somme des angles d'un triangle et unicité de la parallèle : une preuve d'équivalence formalisée en CoqLes vingt-septièmes Journées Francophones des Langages Applicatifs (JFLA 2016), Jade Algave; Julien Signoles, Jan 2016, Saint Malo, France. pp.15
Communication dans un congrès
hal-01228612v2
|