| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
Using small scale automation to improve both accessibility and readability of formal proofs in geometry
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.
Cited literature [33 references]
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
Long-term archiving on: : Thursday, September 25, 2014 - 10:42:05 AM
Contributor : Julien Narboux <>
Submitted on : Wednesday, June 25, 2014 - 9:40:41 AM
Last modification on : Saturday, October 27, 2018 - 1:26:52 AM
Long-term archiving on: : Thursday, September 25, 2014 - 10:42:05 AM
File
small-scale-automation-Tarski-...
Files produced by the author(s)