Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism

DOI10.1007/978-3-642-22863-6_21zbMath1342.68298OpenAlexW1714534555MaRDI QIDQ3088012

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

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

Related Items

A proof system for graph (non)-isomorphism verification ⋮ A FORMAL PROOF OF THE KEPLER CONJECTURE ⋮ Verifying Faradžev-Read Type Isomorph-Free Exhaustive Generation ⋮ Locales: a module system for mathematical theories

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Sphere packings. VI: Tame graphs and linear programs
• Partial and nested recursive function definitions in higher-order logic
• Isabelle/HOL. A proof assistant for higher-order logic
• Flyspeck II: The basic linear programs
• Study of the Kepler's conjecture: the problem of the closest packing
• HOL Light: An Overview
• Code Generation via Higher-Order Rewrite Systems
• Flyspeck I: Tame Graphs
• Programming Languages and Systems
• The Isabelle Collections Framework
• Interpretation of Locales in Isabelle: Theories and Proof Contexts