scientific article; zbMATH DE number 1927415

MaRDI QIDQ4484332zbMATH OpenFDO

Authors Gertrud Bauer, Tobias Nipkow

Publication date 12 June 2003

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2410/24100067.htm

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Coloring of graphs and hypergraphs (05C15)

Recommendations

• The Four Colour Theorem: Engineering of a Formal Proof
• Formal proof - the four color theorem
• scientific article; zbMATH DE number 1021588
• The four-colour theorem
• scientific article; zbMATH DE number 3891395

Cited in

(8)

• A graph library for Isabelle
• Graph theory in Coq: minors, treewidth, and isomorphisms
• Design and formal proof of a new optimal image segmentation program with hypermaps
• Proof pearl: a probabilistic proof for the girth-chromatic number theorem
• Reasoning about cardinalities of relations with applications supported by proof assistants
• On planarity of graphs in homotopy type theory
• 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

Describes a project that uses

Uses Software

• Isabelle/HOL
• Isabelle/Isar
• Isabelle

This page was built for publication:

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