Formal specification and proofs for the topology and classification of combinatorial surfaces |
| |
Institution: | Laboratoire ICUBE, Université de Strasbourg, CNRS, Pôle d''Innovation Technologique, boulevard S. Brant, BP10413, 67400 Illkirch, France |
| |
Abstract: | We describe one of the first attempts at using modern specification techniques in the field of geometric modeling and computational geometry. Using the Coq system, we developed a formal multi-level specification of combinatorial maps, used to represent subdivisions of geometric manifolds, and then exploited it to formally prove fundamental theorems. In particular, we outline here an original and constructive proof of a combinatorial part of the famous Surface Classification Theorem, based on a set of so-called “conservative” elementary operations on subdivisions. |
| |
Keywords: | Combinatorial surfaces Classification Generalized maps Formal specification Assisted proof |
本文献已被 ScienceDirect 等数据库收录! |
|