| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
A combination of a dynamic geometry software with a proof assistant for interactive formal proofs
Abstract : This paper presents an interface for geometry proving. It is a combination of a dynamic geometry software - Geogebra[11] with a proof assistant - Coq[8]. Thanks to the features of Geogebra, users can create and manipulate geometric constructions, they discover conjectures and interactively build formal proofs with the support of Coq. Our system allows users to construct fully traditional proofs in the same style as the ones in high school. For each step of proving, we provide a set of applicable rules veri ed in Coq for users, we also provide tactics in Coq by which minor steps of reasoning are solved automatically.
Cited literature [11 references]
https://hal.inria.fr/inria-00585400
Contributor : Tuan Minh Pham <>
Submitted on : Tuesday, April 12, 2011 - 5:21:43 PM
Last modification on : Thursday, January 7, 2021 - 3:40:09 PM
Long-term archiving on: : Wednesday, July 13, 2011 - 2:48:44 AM
Contributor : Tuan Minh Pham <>
Submitted on : Tuesday, April 12, 2011 - 5:21:43 PM
Last modification on : Thursday, January 7, 2021 - 3:40:09 PM
Long-term archiving on: : Wednesday, July 13, 2011 - 2:48:44 AM
File
paper8.pdf
Files produced by the author(s)