A short note about case distinctions in Tarski's geometry - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2014

A short note about case distinctions in Tarski's geometry

Pierre Boutry
  • Fonction : Auteur
  • PersonId : 2808
  • IdHAL : boutry
IGG
Pascal Schreck
  • Fonction : Auteur
  • PersonId : 864753
IGG
Gabriel Braun
  • Fonction : Auteur
  • PersonId : 938359
IGG

Résumé

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.
Fichier principal
Vignette du fichier
Tarski_case_distinction_proceedings.pdf (177.13 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00989785 , version 1 (12-05-2014)
hal-00989785 , version 2 (25-06-2014)

Identifiants

  • HAL Id : hal-00989785 , version 2

Citer

Pierre Boutry, Julien Narboux, Pascal Schreck, Gabriel Braun. A short note about case distinctions in Tarski's geometry. Automated Deduction in Geometry 2014, Jul 2014, Coimbra, Portugal. pp.1-15. ⟨hal-00989785v2⟩
354 Consultations
481 Téléchargements

Partager

Gmail Facebook X LinkedIn More