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

No abstract is available for this paper.

• Publication year

  2007

• Venue

  Pattern Recognition

• Publication date

  2007-11-01

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1016/j.patcog.2007.02.013
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• A hypermap framework for computer-aided proofs in surface subdivisions: genus theorem and Euler's formula

  2007cited by this paper
• Contains and inside relationships within combinatorial pyramids

  2006cited by this paper
• nD generalized map pyramids: Definition, representations and basic operations

  2006cited by this paper
• Reversible Polygonalization of a 3D Planar Discrete Curve: Application on Discrete Surfaces

  2005cited by this paper
• A Lattice Approach to Image Segmentation

  2005influential reference
• A computer-checked proof of the Four Colour Theorem

  2005cited by this paper
• Topological model for two-dimensional image representation: definition and optimal extraction algorithm

  2004influential reference
• Interactive Theorem Proving and Program Development

  2004cited by this paper
• Formalizing the trading theorem in Coq

  2004cited by this paper
• Mechanical Theorem Proving in Computational Geometry

  2004cited by this paper
• The 5 Colour Theorem in Isabelle/Isar

  2002cited by this paper
• Formalizing Convex Hulls Algorithms

  2001cited by this paper
• Définition et étude d'un modèle topologique minimal de représentation d'images 2d et 3d. (Definition and study of a minimal topological model of 2d and 3d image representation)

  2001influential reference
• Formalizing Convex Hull Algorithms

  2001cited by this paper
• The design and implementation of panar maps in CGAL

  2000cited by this paper
• Formalizing mathematics in higher-order logic: A case study in geometric modelling

  2000cited by this paper
• Functional specification and prototyping with oriented combinatorial maps

  2000cited by this paper
• Representation of segmented images with discrete geometric maps

  1999cited by this paper
• The Design and Implementation of Planar Maps in CGAL

  1999cited by this paper
• Border Map: A Topological Representation for nD Image Analysis

  1999cited by this paper
• The Coq proof assistant : reference manual, version 6.1

  1997cited by this paper
• The Coq Proof Assistant : A Tutorial : Version 7.2

  1997cited by this paper
• Algebraic Specification of a 3D-Modeler Based on Hypermaps

  1994cited by this paper
• Inductive Definitions in the system Coq - Rules and Properties

  1993cited by this paper
• Axioms and Hulls

  1992cited by this paper
• Topological models for boundary representation: a comparison with n-dimensional generalized maps

  1991cited by this paper
• Marching cubes: A high resolution 3D surface construction algorithm

  1987cited by this paper
• Constructions: A Higher Order Proof System for Mechanizing Mathematics

  1985cited by this paper
• Image Segmentation Techniques

  1984cited by this paper
• Representations for Rigid Solids: Theory, Methods, and Systems

  1980cited by this paper
• Digital Picture Processing

  1976cited by this paper
• Un code pour les graphes planaires et ses applications

  1973cited by this paper
• ON IMAGE SEGMENTATION TECHNIQUES

  year unknowncited by this paper

• Merge-and-simplify operation for compact combinatorial pyramid definition

  2020cites this paper
• Tests and proofs for custom data generators

  2018cites this paper
• Tests and Proofs for Enumerative Combinatorics

  2016cites this paper
• Formal study of functional orbits in finite domains

  2015cites this paper
• Designing and proving correct a convex hull algorithm with hypermaps in Coq

  2012cites this paper
• Formal Proof in Coq and Derivation of an Imperative Program to Compute Convex Hulls

  2012cites this paper
• Preuves formelles pour le calcul d'enveloppes convexes dans le plan avec des hypercartes

  2010cites this paper
• Formal Study of Plane Delaunay Triangulation

  2010cites this paper
• An Intuitionistic Proof of a Discrete Form of the Jordan Curve Theorem Formalized in Coq with Combinatorial Hypermaps

  2009cites this paper
• Formalizing Desargues' theorem in Coq using ranks

  2009cites this paper
• Discrete Jordan Curve Theorem: A proof formalized in Coq with hypermaps

  2008cites this paper
• Constructive Mathematics and Functional Programming (Abstract)

  2008cites this paper
• Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof

  2008cites this paper
• HABILITATION A DIRIGER LES RECHERCHES

  2007cites this paper
• Mechanical Theorem Proving in Tarski's Geometry

  2006cites this paper