Formalizing mathematics in higher-order logic: A case study in geometric modelling

✍ Scribed by François Puitg; Jean-François Dufourd

• Publisher: Elsevier Science
• Year: 2000
• Tongue: English
• Weight: 421 KB
• Volume: 234
• Category: Article
• ISSN: 0304-3975
• DOI: 10.1016/s0304-3975(98)00228-x

✦ Synopsis

An innovative attempt to develop formal techniques of speciÿcation, proof, and program extraction in geometric modelling is reported through the axiomatization of the mathematical model of the combinatorial maps in the calculus of inductive constructions (CIC), a variety of type theory well suited for mechanizing mathematics in higher-order logic. A hierarchical speciÿcation of ordered sorts is presented and validated by inductive proofs of consistency and completeness in the Coq system, a prover built on CIC. Automatic extraction of functional algorithms from constructive proofs is investigated through the development of a prototype. Classical di culties in formal speciÿcation and theorem proving -like cohabitation of objects with their generalization in the same hierarchy, smooth handling of subtyping, completion of partial relations or objects, observationality vs. constructivism, and symmetry of relations -are addressed, not only at the formal speciÿcation and theorem proving level but also from the prototyping viewpoint. Geometrical modelling issues are thus solved in a new and unquestionable fashion, giving a great insight on the domain and a deep understanding of the model. A methodology of formal program development that could apply to other areas of computer science is then proposed.