Using small scale automation to improve both accessibility and readability of formal proofs in 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

Using small scale automation to improve both accessibility and readability of formal proofs in 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é

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

Dates et versions

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

Identifiants

  • HAL Id : hal-00989781 , version 2

Citer

Pierre Boutry, Julien Narboux, Pascal Schreck, Gabriel Braun. Using small scale automation to improve both accessibility and readability of formal proofs in geometry. Automated Deduction in Geometry 2014, Jul 2014, Coimbra, Portugal. pp.1-19. ⟨hal-00989781v2⟩
452 Consultations
407 Téléchargements

Partager

Gmail Facebook X LinkedIn More