A graph library for Isabelle

DOI10.1007/s11786-014-0183-zzbMath1308.05055OpenAlexW2044116584MaRDI QIDQ2018659

Lars Noschinski

Publication date: 25 March 2015

Published in: Mathematics in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s11786-014-0183-z

zbMATH Keywords

graph theoryEulerHOLIsabelleKuratowski

Mathematics Subject Classification ID

Directed graphs (digraphs), tournaments (05C20) Eulerian and Hamiltonian graphs (05C45)

Related Items (14)

A modular first formalisation of combinatorial design theory ⋮ Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms ⋮ Introduction to graph enumerations ⋮ About regular graphs ⋮ Isabelle formalisation of original representation theorems ⋮ Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Graph theory in Coq: minors, treewidth, and isomorphisms ⋮ Unnamed Item ⋮ Formalizing network flow algorithms: a refinement approach in Isabelle/HOL ⋮ Trustworthy Graph Algorithms (Invited Talk) ⋮ Infeasible Paths Elimination by Symbolic Execution Techniques ⋮ Formalizing the Edmonds-Karp Algorithm

Uses Software

• ACL2
• Isabelle
• LEDA
• Isabelle/HOL
• HOL
• Flyspeck
• Locales
• Dijkstra Shortest Path
• Tame Graphs
• Graph Theory
• NASA PVS
• CAVA LTL Modelchecker
• AutoCorres

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Isabelle/HOL. A proof assistant for higher-order logic
• A framework for the verification of certifying computations
• Locales: a module system for mathematical theories
• Flyspeck I: Tame Graphs
• Meta Reasoning in ACL2
• Digraphs

This page was built for publication: A graph library for Isabelle