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

DOI10.1016/S0304-3975(98)00228-XzbMath0945.68178OpenAlexW2027604973MaRDI QIDQ1575663

F. Puitg, Jean-François Dufourd

Publication date: 21 August 2000

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(98)00228-x

zbMATH Keywords

theorem provingprogram extractionformal specificationsgeometric modellinginductive proofscoq

Mathematics Subject Classification ID

Computer graphics; computational geometry (digital and algorithmic aspects) (68U05) Abstract data types; algebraic specification (68Q65)

Related Items

Verification of Closest Pair of Points Algorithms, Design and formal proof of a new optimal image segmentation program with hypermaps, Formal specification and proofs for the topology and classification of combinatorial surfaces, Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof

Uses Software

• Coq

Cites Work

• Classification of the genus-1 rooted maps and associated functional relation
• Topological models for boundary representation: A comparison with \(n\)- dimensional generalized maps
• Behavioural approaches to algebraic specifications. A comparative study
• Combinatorial Oriented Maps
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item