Abstract
We study the formalization and then the proof of a well-known theorem of surface topology called the trading theorem. This is the first major work undertaken with our Coq specification of the generalized maps, which may be used as a model for surfaces subdivisions. We explain how we expressed in terms of subdivisions the notion of topological equivalence, and how we used this notion to prove the trading theorem, while giving a quick look at the specification we have built.
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.
Similar content being viewed by others
References
Barras, B. et al.: The Coq proof assistant reference manual. http://coq.inria.fr/doc/main.html
Bertrand, G., Malgouyres, R.: Some topological properties of surfaces in Z3. Journal of Mathematical Imaging and Vision no 11 (1999) 207–221
Bertrand, Y., Dufourd, J.-F.: Algebraic specification of a 3D-modeler based on hypermaps. Graphical Models and Image Processing (1994) 56(1) 29–60
Coquand, T., Huet, G.: Constructions: a higher order proof system for mechanizing mathematics. EUROCAL (1985) Springer-Verlag LNCS 203
Cori, R.: Un Code pour les Graphes Planaires et ses Applications. Société Math. de France, Astérisque 27 (1970)
Dehlinger, C, Dufourd, J.-F., Schreck, P.: Higher-Order Intuitionistic Formalization and Proofs in Hubert’s Elementary Geometry. Automated Deduction in Geometry (2000) Springer-Verlag LNAI 2061
Firby, P. A., Gardiner, C. F.: Surface Topology. Ellis Horwood Ltd. (1982)
Fomenko, A. T.: Differential Geometry and Topology. Consultant Associates (1987)
Griffiths, H.: Surfaces. Cambridge University Press (1981)
Jacques, A.: Constellations et graphes topologiques. Combinatorial Theory And Applications (1970) 657–673
Kahn, G.: Elements of Constructive Geometry, Group Theory, and Domain Theory. Coq contribution (http://coq.inria.fr/contribs-eng.html)
Knuth, D.E.: Axioms and Hulls. Springer-Verlag (1992) LNCS 606
Lienhardt, P.: Subdivisions of N-Dimensional Spaces and N-Dimensional Generalized Maps. Computational Geometry ACM Symp. (1989) 228–236
Martin-Löf, P.: Intuitionistic Type Theory. Bibliopolis (1984)
Parent, C: Synthesizing proofs from programs in the calculus of inductive constructions. Mathematics of Program Construction (1995) Springer-Verlag LNCS 947
Pichardie, D., Bertot, Y.: Formalizing Convex Hulls Algorithms. TPHOL (2001) Springer-Verlag LNCS 2152 346–361
Puitg, F., Dufourd, J.-F.: Formal specifications and theorem proving breakthroughs in geometric modelling. TPHOL (1998) Springer-Verlag LNCS 1479 401–427
Von Plato, J.: The axioms of constructive geometry. Annals of pure and applied logic 76 (1995) 169–200
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dehlinger, C., Dufourd, JF. (2002). Formalizing the Trading Theorem for the Classification of Surfaces. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2002. Lecture Notes in Computer Science, vol 2410. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45685-6_11
Download citation
DOI: https://doi.org/10.1007/3-540-45685-6_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44039-0
Online ISBN: 978-3-540-45685-8
eBook Packages: Springer Book Archive