Výsledky vyhledávání - "neutral geometry"

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

Zobrazit plný text záznamu

A Synthetic Proof of Pappus’ Theorem in Tarski’s Geometry

Autor: Gabriel Braun, Julien Narboux

Publikováno v: Journal of Automated Reasoning
Journal of Automated Reasoning, Springer Verlag, 2017, 58 (2), pp.23. ⟨10.1007/s10817-016-9374-4⟩
Journal of Automated Reasoning, 2017, 58 (2), pp.23. ⟨10.1007/s10817-016-9374-4⟩

International audience; In this paper, we report on the formalization of a synthetic proof of Pappus' theorem. We provide two versions of the theorem: the first one is proved in neutral geometry (without assuming the parallel postulate), the second (

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7977d8284fd5f632849f3a8fc40dcce3
https://doi.org/10.1007/s10817-016-9374-4

Zobrazit plný text záznamu

GeoCoq

Autor: Beeson, Michael, Boutry, Pierre, Braun, Gabriel, Gries, Charly, Narboux, Julien

Publikováno v: 2018, ⟨swh:1:dir:97ce53176b7d5e89d069bc60f49c3fa186831307;origin=https://hal.archives-ouvertes.fr/hal-01912024;visit=swh:1:snp:1cbf6e8cee9dde43b03c16566f00122653381227;anchor=swh:1:rev:640e8d6a4813be6b44bee473dfb674f40daac1f0;path=/⟩

A formalization of geometry in Coq.This library contains a formalization of geometry using the Coq proof assistant. It contains both proofs about the foundations of geometry and high-level proofs in the same style as in high-school.

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=od______1398::f17ab6ebcf9eba78f0cb7677f0cb948f
https://hal.inria.fr/hal-01912024

Zobrazit plný text záznamu

Dissertation/ Thesis

Introdução à geometria hiperbólica

Autor: Valério, José Carlos

Publikováno v: Repositório Institucional da UFJFUniversidade Federal de Juiz de ForaUFJF.

Submitted by Renata Lopes (renatasil82@gmail.com) on 2017-07-03T19:23:35Z No. of bitstreams: 1 josecarlosvalerio.pdf: 982623 bytes, checksum: 72d4cd36b83464bfd6a83caee289315d (MD5)
Approved for entry into archive by Adriana Oliveira (adriana.oli

Externí odkaz: https://repositorio.ufjf.br/jspui/handle/ufjf/5405

Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání