Abstract
We present in this paper the development of a decision procedure for affine plane geometry in the Coq proof assistant. Among the existing decision methods, we have chosen to implement one based on the area method developed by Chou, Gao and Zhang, which provides short and “readable” proofs for geometry theorems. The idea of the method is to express the goal to be proved using three geometric quantities and eliminate points in the reverse order of their construction thanks to some elimination lemmas.
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
Boutin, S.: Using reflection to build efficient and certified decision procedures. In: Ito, T., Abadi, M. (eds.) TACS 1997. LNCS, vol. 1281, Springer, Heidelberg (1997)
Chou, S.C., Gao, X.S., Zhang, J.Z.: Machine Proofs in Geometry. World Scientific, Singapore (1994)
Chou, S.-C.: Mechanical Geometry Theorem Proving. D. Reidel Publishing Company (1988)
Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975)
Dehlinger, C., Dufourd, J.-F., Schreck, P.: Higher-order intuitionistic formalization and proofs in Hilbert’s elementary geometry. In: Automated Deduction in Geometry, pp. 306–324 (2000)
Euclide. Les éléments. Presses Universitaires de France (1998), Traduit par Bernard Vitrac
Guilhot, F.: Formalisation en coq d’un cours de géométrie pour le lycée. Journées Francophones des Langages Applicatifs (Janvier 2004)
Guilhot, F., Narboux, J.: Toward a “common” language for formally stating elementary geometry theorems. Draft
Harrison, J.: Meta theory and reflection in theorem proving:a survey and critique. Technical Report CRC-053, SRI International Cambridge Computer Science Research Center (1995)
Hilbert, D.: Les fondements de la géométrie. Dunod, Paris, Jacques Gabay edition (1971), Edition critique avec introduction et compléments préparée par Paul Rossier
Howe, D.: Computation meta theory in nuprl. In: Lusk, E.‘., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 238–257. Springer, Heidelberg (1988)
Kahn, G.: Constructive geometry according to Jan von Plato. Coq contribution. Coq V5.10
The Coq development team. The Coq proof assistant reference manual. LogiCal Project, Version 8.0 (2004)
Meikle, L.I., Fleuriot, J.D.: Formalizing Hilbert’s grundlagen in isabelle/ isar. Theorem Proving in Higher Order Logics, 319–334 (2003)
Tarski, A.: A decision method for elementary algebra and geometry. University of California Press (1951)
Tarski, A.: What is elementary geometry? In: Suppes, P., Henkin, L., Tarski, A. (eds.) The axiomatic Method, with special reference to Geometry and Physics, pp. 16–29. North-Holland, Amsterdam (1959)
von Plato, J.: The axioms of constructive geometry. Annals of Pure and Applied Logic 76, 169–200 (1995)
Wu, W.-T.: On the decision problem and the mechanization of theorem proving in elementary geometry. Scientia Sinica 21, 157–179 (1978)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Narboux, J. (2004). A Decision Procedure for Geometry in Coq. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2004. Lecture Notes in Computer Science, vol 3223. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30142-4_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-30142-4_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23017-5
Online ISBN: 978-3-540-30142-4
eBook Packages: Springer Book Archive