Design and formal proof of a new optimal image segmentation program with hypermaps

DOI10.1016/J.PATCOG.2007.02.013MaRDI QIDQ2643883zbMATH OpenOpenAlexFDO

Authors Jean-François Dufourd

Publication date 27 August 2007

Published in Pattern Recognition (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.patcog.2007.02.013

zbMATH Keywords

image segmentationformal specificationCoq systemhypermapscomputer-aided correctness proof

Mathematics Subject Classification ID

Pattern recognition, speech recognition (68T10) Computing methodologies for image processing (68U10) Theory of software (68N99)

Recommendations

• Designing and proving correct a convex hull algorithm with hypermaps in Coq
• Formal proof in Coq and derivation of an imperative program to compute convex hulls
• Graph-Based Representations in Pattern Recognition
• Functional specification and prototyping with oriented combinatorial maps
• Fast Constrained Image Segmentation Using Optimal Spanning Trees

Cites work

• scientific article; zbMATH DE number 3900666 (Why is no real title available?)
• scientific article; zbMATH DE number 3928956 (Why is no real title available?)
• scientific article; zbMATH DE number 3489159 (Why is no real title available?)
• scientific article; zbMATH DE number 512790 (Why is no real title available?)
• scientific article; zbMATH DE number 1927415 (Why is no real title available?)
• scientific article; zbMATH DE number 1863395 (Why is no real title available?)
• A lattice approach to image segmentation
• Automated Deduction in Geometry
• Axioms and hulls
• Contains and inside relationships within combinatorial pyramids
• Discrete Geometry for Computer Imagery
• Formalizing mathematics in higher-order logic: A case study in geometric modelling
• Formalizing the trading theorem in Coq
• Functional specification and prototyping with oriented combinatorial maps
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Topological models for boundary representation: A comparison with \(n\)- dimensional generalized maps
• \(n\)D generalized map pyramids: definition, representations and basic operations

Cited in

(8)

• Designing and proving correct a convex hull algorithm with hypermaps in Coq
• An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps
• Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof
• Tests and proofs for custom data generators
• Mechanical Theorem Proving in Tarski’s Geometry
• Formal study of functional orbits in finite domains
• Constructive Mathematics and Functional Programming (Abstract)
• Tests and Proofs for Enumerative Combinatorics

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Design and formal proof of a new optimal image segmentation program with hypermaps

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