A graph library for Isabelle

DOI10.1007/S11786-014-0183-ZzbMATH Open1308.05055OpenAlexW2044116584MaRDI QIDQ2018659FDOQ2018659

Authors 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)

Recommendations

• Graph theory in Coq: minors, treewidth, and isomorphisms
• scientific article; zbMATH DE number 1927415
• Miscellaneous graph preliminaries
• scientific article; zbMATH DE number 3845636

Cites Work

• scientific article; zbMATH DE number 3458642 (Why is no real title available?)
• scientific article; zbMATH DE number 1368469 (Why is no real title available?)
• scientific article; zbMATH DE number 843316 (Why is no real title available?)
• A framework for the verification of certifying computations
• Digraphs
• Flyspeck I: Tame Graphs
• Graph theory
• Isabelle/HOL. A proof assistant for higher-order logic
• Locales: a module system for mathematical theories
• Meta Reasoning in ACL2

Cited In (20)

• Graph theory in Coq: minors, treewidth, and isomorphisms
• Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms
• A proof system for graph (non)-isomorphism verification
• The Isabelle Framework
• A modular first formalisation of combinatorial design theory
• Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL
• Infeasible paths elimination by symbolic execution techniques. Proof of correctness and preservation of paths
• Trustworthy Graph Algorithms (Invited Talk)
• About regular graphs
• Miscellaneous graph preliminaries. I
• Formalising the double-pushout approach to graph transformation
• Introduction to graph enumerations
• Towards mechanised proofs in double-pushout graph transformation
• Miscellaneous graph preliminaries
• Mechanised DPO theory: uniqueness of derivations and Church-Rosser theorem
• Title not available (Why is no real title available?)
• Title not available (Why is no real title available?)
• Isabelle formalisation of original representation theorems
• Formalizing the Edmonds-Karp algorithm
• Formalizing network flow algorithms: a refinement approach in Isabelle/HOL

Uses Software

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

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

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