Using small scale automation to improve both accessibility and readability of formal proofs in 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 : This paper describes some techniques to help building formal proofs in geometry and at the same time improving readability. Rather than trying to completely automate the proving process we provide symbolic manipulations which are useful to automate the parts of the formal proof that are usually implicit in a pen and paper proof. We test our framework using some well known theorems about triangles which are taught in high-school. We also highlight the proof steps which are usually overlooked in the informal proof and that we believe should be made explicit. Our framework is based on Tarski's geometry within the Coq proof assistant, but most of the ideas presented in this paper could be applied to other axiomatic systems or proof assistants.
Keywords : 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-19, 2014, Proceedings of ADG 2014
Liste complète des métadonnées

Littérature citée [33 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-00989781
Contributeur : Julien Narboux <>
Soumis le : mercredi 25 juin 2014 - 09:40:41
Dernière modification le : samedi 27 octobre 2018 - 01:26:52
Document(s) archivé(s) le : jeudi 25 septembre 2014 - 10:42:05

Fichier

small-scale-automation-Tarski-...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00989781, version 2

Collections

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

Citation

Pierre Boutry, Julien Narboux, Pascal Schreck, Gabriel Braun. Using small scale automation to improve both accessibility and readability of formal proofs in geometry. Francisco Botana and Pedro Quaresma. Automated Deduction in Geometry 2014, Jul 2014, Coimbra, Portugal. pp.1-19, 2014, Proceedings of ADG 2014. 〈hal-00989781v2〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

577

Téléchargements de fichiers

330

Contact


archive-ouverte@inria.fr