Abstract
In this article, we present the development of a library of formal proofs for theorem proving in plane geometry in a pedagogical context. We use the Coq proof assistant [4]. This library includes the basic geometric notions to state theorems and provides a database of theorems to construct interactive proofs more easily. It is an extension of the library of F. Guilhot for interactive theorem proving at the level of high-school geometry [7], where we eliminate redundant axioms and give formalizations for the geometric concepts using a vector approach. We also enrich this library by offering an automated deduction method which can be used as a complement to interactive proof. For that purpose, we integrate the formalization of the area method [3] which was developed by J. Narboux in Coq [12, 10].
This work is partially supported by the french ANR project Galapagos.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Berger, M., Pansu, P., Berry, J.P., Saint-Raymond, X.: Problems in Geometry. Springer, Heidelberg (1984)
Bertot, Y., Guilhot, F., Pottier, L.: Visualizing Geometrical Statements with GeoView. Electronic Notes in Theoretical Computer Science 103, 49–65 (2003)
Chou, S.C., Gao, X.S., Zhang, J.Z.: Machine Proofs in Geometry. World Scientific, Singapore (1994)
Coq development team: The Coq Proof Assistant Reference Manual, Version 8.3. TypiCal Project (2010), http://coq.inria.fr
Dehlinger, C., Dufourd, J.-F., Schreck, P.: Higher-Order Intuitionistic Formalization and Proofs in Hilbert’s Elementary Geometry. In: Richter-Gebert, J., Wang, D. (eds.) ADG 2000. LNCS (LNAI), vol. 2061, pp. 306–324. Springer, Heidelberg (2001)
Geogebra development team: Introduction to GeoGebra, http://www.geogebra.org/book/intro-en/
Guilhot, F.: Formalisation en Coq et visualisation d’un cours de géométrie pour le lycée. TSI 24, 1113–1138 (2005) (in french)
Hilbert, D.: Les fondements de la géométrie. In: Gabay, J. (ed.) Edition critique avec introduction et compléments préparée par Paul Rossier. Dunod, Paris (1971)
Janicić, P.: Geometry construction language. Journal of Automated Reasoning 44, 3–24 (2010)
Janicic, P., Narboux, J., Quaresma, P.: The Area Method: a Recapitulation. Journal of Automated Reasoning (2010)
Meikle, L., Fleuriot, J.: Formalizing Hilbert’s Grundlagen in Isabelle/Isar. In: Theorem Proving in Higher Order Logics, pp. 319–334 (2003)
Narboux, J.: A Decision Procedure for Geometry in Coq. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 225–240. Springer, Heidelberg (2004)
Narboux, J.: Toward the use of a proof assistant to teach mathematics. In: Proceedings of the 7th International Conference on Technology in Mathematics Teaching, ICTMT 7 (2005)
Narboux, J.: A graphical user interface for formal proofs in geometry. J. Autom. Reasoning 39(2), 161–180 (2007)
Narboux, J.: Mechanical Theorem Proving in Tarski’s Geometry. In: Botana, F., Recio, T. (eds.) ADG 2006. LNCS (LNAI), vol. 4869, pp. 139–156. Springer, Heidelberg (2007)
Pham, T.-M., Bertot, Y.: A combination of a dynamic geometry software with a proof assistant for interactive formal proofs. In: UITP Workshops 2010 (2010)
Scott, P., Fleuriot, J.: Idle time discovery in geometry theorem proving. In: Proceedings of ADG 2010 (2010)
Tarski, A.: What is Elementary Geometry?. In: Henkin, L., Suppes, P., Tarski, A. (eds.) The axiomatic Method, with special reference to Geometry and Physics, pp. 16–29. North-Holland, Amsterdam (1959)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pham, TM., Bertot, Y., Narboux, J. (2011). A Coq-Based Library for Interactive and Automated Theorem Proving in Plane Geometry. In: Murgante, B., Gervasi, O., Iglesias, A., Taniar, D., Apduhan, B.O. (eds) Computational Science and Its Applications - ICCSA 2011. ICCSA 2011. Lecture Notes in Computer Science, vol 6785. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21898-9_32
Download citation
DOI: https://doi.org/10.1007/978-3-642-21898-9_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21897-2
Online ISBN: 978-3-642-21898-9
eBook Packages: Computer ScienceComputer Science (R0)