Design and formal proof of a new optimal image segmentation program with hypermaps
From MaRDI portal
Publication:2643883
DOI10.1016/J.PATCOG.2007.02.013zbMATH Open1118.68725OpenAlexW2082102386MaRDI QIDQ2643883FDOQ2643883
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
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
Pattern recognition, speech recognition (68T10) Computing methodologies for image processing (68U10) Theory of software (68N99)
Cites Work
- A lattice approach to image segmentation
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Axioms and hulls
- Title not available (Why is that?)
- Title not available (Why is that?)
- Topological models for boundary representation: A comparison with \(n\)- dimensional generalized maps
- Formalizing mathematics in higher-order logic: A case study in geometric modelling
- Functional specification and prototyping with oriented combinatorial maps
- Formalizing the trading theorem in Coq
- Title not available (Why is that?)
- Title not available (Why is that?)
- Automated Deduction in Geometry
- Title not available (Why is that?)
- Title not available (Why is that?)
- \(n\)D generalized map pyramids: definition, representations and basic operations
- Contains and inside relationships within combinatorial pyramids
- Discrete Geometry for Computer Imagery
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
Uses Software
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)
