×

A combination of a dynamic geometry software with a proof assistant for interactive formal proofs. (English) Zbl 1294.68126

Aspinall, David (ed.) et al., Proceedings of the 9th international workshop on user interfaces for theorem provers (UITP10), Edinburgh, UK, July 15, 2010. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 285, 43-55 (2012).
Summary: This paper presents an interface for geometry proving. It is a combination of a dynamic geometry software Geogebra with the proof assistant Coq. 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.
For the entire collection see [Zbl 1284.68005].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68U05 Computer graphics; computational geometry (digital and algorithmic aspects)
68U35 Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Amerkad, A. and Y. Bertot and L. Pottier and L. Rideau: 2001, Mathematics and Proof Presentation in Pcoq; Amerkad, A. and Y. Bertot and L. Pottier and L. Rideau: 2001, Mathematics and Proof Presentation in Pcoq
[2] Bertot, Y.; Guilhot, F.; Pottier, L., Visualizing Geometrical Statements with GeoView, Electronic Notes in Theoretical Computer Science, 103, 49-65 (2004)
[3] Bertot, Y.; Khan, G.; Théry, L., Proof by pointing. Theoretical Aspects of Computer Software, LNCS, 789, 141-160 (1994)
[4] Chou, S.-C., An introduction to Wuʼs method for mechanical theorem proving in geometry, Journal of Automated Reasoning, 4, 237-267 (1988) · Zbl 0715.03005
[5] Chou, S.-C.; Gao, X.-S.; Zhang, J.-Z., Machine proofs in geometry: Automated production of readable proofs for Geometry Theorems (1994), World Scientific · Zbl 0941.68503
[6] Chou, S.-C.; Gao, X.-S.; Zhang, J.-Z., Automated generation of readable proofs with geometric invariants. Theorem proving with full-angles, Journal of Automated Reasoning, 17, 349-370 (1996) · Zbl 0865.68110
[7] Chou, S.-C.; Gao, X.-S.; Zhang, J.-Z., A deductive database approach to automated geometry theorem proving and discovering, Journal of Automated Reasoning, 25, 219-246 (1996) · Zbl 0961.68121
[8] Coq development team, The Coq proof assitant reference manual
[9] Gao, X.-S., Geometry Expert, Software Package (2000)
[10] Gao, X.-S. and Q.Lin: 2002, MMP/Geometer - a software package for automated geometry reasoning; Gao, X.-S. and Q.Lin: 2002, MMP/Geometer - a software package for automated geometry reasoning · Zbl 1202.68378
[11] Geogebra development team, Introduction to GeoGebra
[12] Guilhot, F., Formalisation en Coq et visualisation dʼun cours de géométrie pour le lycée, Technique et Science Informatiques, 24, 1113-1138 (2005)
[13] Kapur, D., Using Gröbner Bases to reason about geometry problems, Journal of Symbolic Computation, 2, 399-408 (1986) · Zbl 0629.68087
[14] Narboux, J., A Decision Procedure for Geometry in Coq, (Proceedings of Theorem Proving in Higher-Order Logics. Proceedings of Theorem Proving in Higher-Order Logics, LNCS, vol. 3223 (2004)) · Zbl 1099.68734
[15] Narboux, J., A Graphical User Interface for Formal Proofs in Geometry, Journal of Automated Reasoning, 39, 161-180 (2007) · Zbl 1131.68094
[16] Quaresma, P.; Janičić, P., GeoThms - a Web System for Euclidean Constructive Geometry, Electronic Notes in Theoretical Computer Science, 174, 35-48 (2007) · Zbl 1278.68279
[17] Wilson, S. and Jacques D. Fleuriot: 2005, Combining Dynamic Geometry, Automated Geometry Theorem Proving And Diagrammatic Proofs; Wilson, S. and Jacques D. Fleuriot: 2005, Combining Dynamic Geometry, Automated Geometry Theorem Proving And Diagrammatic Proofs
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.