A short note about case distinctions in Tarski's geometry

Pierre Boutry 1 Julien Narboux 2 Pascal Schreck 1 Gabriel Braun 1
1 IGG
ICube - Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie
2 ICube - Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie
Abstract : In this paper we study some decidability properties in the context of Tarski's axiom system for geometry. We removed excluded middle from our assumptions and studied how our formal proof of the first thirteen chapters of [SST83] are impacted. We show that decidability of equality is equivalent to the decidability of the two other given predicates of the theory: congruence and betweenness. We prove that the decidability of the other predicates used in [SST83] can be derived except for the predicate stating the existence of the intersection of two lines. All results have been proved formally using the Coq proof assistant.
Keywords : decidability formalization geometry Coq proof assistant Tarski
Type de document :
Communication dans un congrès
Francisco Botana and Pedro Quaresma. Automated Deduction in Geometry 2014, Jul 2014, Coimbra, Portugal. pp.1-15, 2014, Proceedings of ADG 2014
Liste complète des métadonnées

Littérature citée [13 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-00989785
Contributeur : Julien Narboux <>
Soumis le : mercredi 25 juin 2014 - 09:36:37
Dernière modification le : jeudi 29 mars 2018 - 09:10:05
Document(s) archivé(s) le : jeudi 25 septembre 2014 - 10:41:54

Fichier

Tarski_case_distinction_procee...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00989785, version 2

Collections

INSA-STRASBOURG | GEOCOQ | INC-CNRS | SITE-ALSACE

Citation

Pierre Boutry, Julien Narboux, Pascal Schreck, Gabriel Braun. A short note about case distinctions in Tarski's geometry. Francisco Botana and Pedro Quaresma. Automated Deduction in Geometry 2014, Jul 2014, Coimbra, Portugal. pp.1-15, 2014, Proceedings of ADG 2014. 〈hal-00989785v2〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

508

Téléchargements de fichiers

318

Contact


archive-ouverte@inria.fr