Verified efficient enumeration of plane graphs modulo isomorphism

DOI10.1007/978-3-642-22863-6_21MaRDI QIDQ3088012zbMATH OpenOpenAlexFDO

Authors Tobias Nipkow

Publication date 17 August 2011

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-22863-6_21

Mathematics Subject Classification ID

Isomorphism problems in graph theory (reconstruction conjecture, etc.) and homomorphisms (subgraph embedding, etc.) (05C60) Enumeration in graph theory (05C30) Packing and covering in (n) dimensions (aspects of discrete geometry) (52C17) Combinatorial aspects of packing and covering (05B40)

Recommendations

• Flyspeck I: Tame Graphs
• scientific article; zbMATH DE number 2209729
• Sphere packings. VI: Tame graphs and linear programs
• A revision of the proof of the Kepler conjecture
• scientific article; zbMATH DE number 1789934

Cites work

• Code generation via higher-order rewrite systems
• Dense sphere packings. A blueprint for formal proofs
• Flyspeck I: Tame Graphs
• Flyspeck II: The basic linear programs
• HOL Light: An Overview
• Interpretation of Locales in Isabelle: Theories and Proof Contexts
• Isabelle/HOL. A proof assistant for higher-order logic
• Partial and nested recursive function definitions in higher-order logic
• Programming Languages and Systems
• Sphere packings. VI: Tame graphs and linear programs
• Study of the Kepler's conjecture: the problem of the closest packing
• The Isabelle collections framework
• Tutorial to locales and locale interpretation

Cited in

(7)

• A proof system for graph (non)-isomorphism verification
• A formal proof of the Kepler conjecture
• Flyspeck I: Tame Graphs
• Gale-Shapley verified
• Verifying Faradžev-Read Type Isomorph-Free Exhaustive Generation
• Locales: a module system for mathematical theories
• Efficient enumeration of non-isomorphic Ptolemaic graphs

Describes a project that uses

Uses Software

• Archive Formal Proofs
• Tame Graphs
• Jinja Threads
• Locales
• Flyspeck
• HOL Light
• Isabelle/HOL
• Isabelle

This page was built for publication: Verified efficient enumeration of plane graphs modulo isomorphism

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