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
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [33 references]  Display  Hide  Download
https://hal.inria.fr/hal-00989781
Contributor : Julien Narboux <>
Submitted on : Wednesday, June 25, 2014 - 9:40:41 AM
Last modification on : Saturday, October 27, 2018 - 1:26:52 AM
Document(s) archivé(s) le : Thursday, September 25, 2014 - 10:42:05 AM

File

small-scale-automation-Tarski-...
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00989781, version 2

Collections

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

Citation

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⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

593

Files downloads

345

Contact


archive-ouverte@inria.fr