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

DOI10.1016/S0304-3975(98)00228-XMaRDI QIDQ1575663zbMATH OpenOpenAlexFDO

Authors 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

coqformal specificationsgeometric modellinginductive proofsprogram extractiontheorem proving

Mathematics Subject Classification ID

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

Recommendations

• Formalization of geometric algebra theories in higher-order logic
• Geometric Models for Relevant Logics
• scientific article; zbMATH DE number 1745043
• Geometrisation of first-order logic
• scientific article; zbMATH DE number 860049
• Foreword. Formalization of geometry, automated and interactive geometric reasoning
• Modal logics of some geometrical structures
• Logical and set calculations in the framework of geometrical informatics paradigm

Cites work

• Behavioural approaches to algebraic specifications. A comparative study
• Classification of the genus-1 rooted maps and associated functional relation
• Combinatorial Oriented Maps
• scientific article; zbMATH DE number 2185702 (Why is no real title available?)
• scientific article; zbMATH DE number 4060701 (Why is no real title available?)
• scientific article; zbMATH DE number 3716440 (Why is no real title available?)
• scientific article; zbMATH DE number 3489159 (Why is no real title available?)
• scientific article; zbMATH DE number 3518832 (Why is no real title available?)
• scientific article; zbMATH DE number 512790 (Why is no real title available?)
• scientific article; zbMATH DE number 1142323 (Why is no real title available?)
• scientific article; zbMATH DE number 3298598 (Why is no real title available?)
• scientific article; zbMATH DE number 3338383 (Why is no real title available?)
• Topological models for boundary representation: A comparison with \(n\)- dimensional generalized maps

Cited in

(5)

• Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm
• 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
• Verification of Closest Pair of Points Algorithms
• Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Formalizing mathematics in higher-order logic: A case study in geometric modelling

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1575663)