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
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.
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

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〉

Partager

Métriques

Consultations de la notice

577

Téléchargements de fichiers

330