Mechanical Theorem Proving in Tarski's geometry.

Julien Narboux 1, 2
2 LOGICAL - Logic and computing
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : This paper describes the mechanization of the proofs of the first height chapters of Schwabäuser, Szmielew and Tarski's book: Metamathematische Methoden in der Geometrie. The goal of this development is to provide foundations for other formalizations of geometry and implementations of decision procedures. We compare the mechanized proofs with the informal proofs. We also compare this piece of formalization with the previous work done about Hilbert's Gründlagen der Geometrie. We analyze the differences between the two axiom systems from the formalization point of view.
Type de document :
Communication dans un congrès
Eugenio Roanes Lozano, Francisco Botana. Automated Deduction in Geometry 2006, Aug 2006, Pontevedra, Spain. Springer, 4869, pp.139-156, 2007, LNCS. 〈10.1007/978-3-540-77356-6〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00118812
Contributeur : Julien Narboux <>
Soumis le : mercredi 6 décembre 2006 - 15:23:38
Dernière modification le : jeudi 10 mai 2018 - 02:06:24
Document(s) archivé(s) le : mardi 6 avril 2010 - 23:56:01

Fichiers

adg06-narboux.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Julien Narboux. Mechanical Theorem Proving in Tarski's geometry.. Eugenio Roanes Lozano, Francisco Botana. Automated Deduction in Geometry 2006, Aug 2006, Pontevedra, Spain. Springer, 4869, pp.139-156, 2007, LNCS. 〈10.1007/978-3-540-77356-6〉. 〈inria-00118812〉

Partager

Métriques

Consultations de la notice

460

Téléchargements de fichiers

295