Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq

Autor: Charly Gries, Pascal Schreck, Pierre Boutry, Julien Narboux

Publikováno v: Journal of Automated Reasoning
Journal of Automated Reasoning, Springer Verlag, 2019, 62 (1), pp.68. ⟨10.1007/s10817-017-9422-8⟩
Journal of Automated Reasoning, 2019, 62 (1), pp.68. ⟨10.1007/s10817-017-9422-8⟩

online first; International audience; In this paper we focus on the formalization of the proofs of equivalence between different versions of Euclid's 5 th postulate. Our study is performed in the context of Tarski's neutral geometry, or equivalently

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::5295cfedebbea0e5f43a1d51340f29ca
https://hal.inria.fr/hal-01178236v2/document

Automated generation of machine verifiable and readable proofs: A case study of Tarski’s geometry

Autor: Sana Stojanović Durdević, Predrag Janičić, Julien Narboux

Publikováno v: Annals of Mathematics and Artificial Intelligence
Annals of Mathematics and Artificial Intelligence, Springer Verlag, 2015, 73 (3), pp.25. ⟨10.1007/s10472-014-9443-5⟩
Annals of Mathematics and Artificial Intelligence, 2015, 73 (3), pp.25. ⟨10.1007/s10472-014-9443-5⟩

International audience; The power of state-of-the-art automated and interactive the-orem provers has reached the level at which a significant portion of non-trivial mathematical contents can be formalized almost fully automat-ically. In this paper we

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7fade1b1841a37754191542e89868753
https://doi.org/10.1007/s10472-014-9443-5

Herbrand's theorem and non-Euclidean geometry

Autor: Pierre Boutry, Michael Beeson, Julien Narboux

Publikováno v: Bulletin of Symbolic Logic
Bulletin of Symbolic Logic, 2015, 21 (2), pp.12. ⟨10.1017/bsl.2015.6⟩
Bulletin of Symbolic Logic, Association for Symbolic Logic, 2015, 21 (2), pp.12. ⟨10.1017/bsl.2015.6⟩

We use Herbrand's theorem to give a new proof that Euclid's parallel axiom is not derivable from the other axioms of first-order Euclidean geometry. Previous proofs involve constructing models of non-Euclidean geometry. This proof uses a very old and

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b21737acf81f388f97ade66b34288d81
http://arxiv.org/abs/1410.2239

Formalising in Nominal Isabelle Crary's Completeness Proof for Equivalence Checking

Autor: Christian Urban, Julien Narboux

Publikováno v: LFMTP'07
LFMTP'07, Jul 2007, Bremen, Germany. 15p., ⟨10.1016/j.entcs.2007.09.014⟩

International audience; In the book on Advanced Topics in Types and Programming Languages, Crary illustrates the reasoning method of logical relations in a case study about equivalence checking. He presents a type-driven equivalence checking algorith

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c05092ccef58506e87e4d6ea26ebc26a
https://hal.inria.fr/inria-00180061v2/document

Formal SOS-Proofs for the Lambda-Calculus

Autor: Christian Urban, Julien Narboux

Publikováno v: Third Workshop on Logical and Semantic Frameworks, with Applications
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⟩
LSFA

International audience; We describe in this paper formalisations for the properties of weakening, type-substitutivity, subject-reduction and termina- tion of the usual big-step evaluation relation. Our language is the lambda-calculus whose simplicity

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a2d035724470a3b5cbcd250f87b6ca5f