Skip to Main content Skip to Navigation
Conference papers

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
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [13 references]  Display  Hide  Download

https://hal.inria.fr/hal-00989785
Contributor : Julien Narboux <>
Submitted on : Wednesday, June 25, 2014 - 9:36:37 AM
Last modification on : Saturday, October 27, 2018 - 1:26:52 AM
Long-term archiving on: : Thursday, September 25, 2014 - 10:41:54 AM

File

Tarski_case_distinction_procee...
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00989785, version 2

Citation

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⟩

Share

Metrics

Record views

614

Files downloads

548