کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
421580 | 684904 | 2012 | 13 صفحه PDF | دانلود رایگان |
This paper presents an interface for geometry proving. It is a combination of a dynamic geometry software, Geogebra [Geogebra development team, Introduction to GeoGebra. http://www.geogebra.org/book/intro-en/] with a proof assistant, Coq [Coq development team, The Coq proof assitant reference manual. http://coq.inria.fr/refman/]. 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 verified in Coq for users, we also provide tactics in Coq by which minor steps of reasoning are solved automatically.
Journal: Electronic Notes in Theoretical Computer Science - Volume 285, 19 September 2012, Pages 43-55