From: "McCue, Brian" <firstname.lastname@example.org>
Can HOL/Isabelle be used with graph theory to prove whether a graph is isomorphic?
(I am a first-year math student and start classes next week. I was installing Python TensorFlow and some libraries led me to HOL/Isabelle).
Thank you for looking at my question above.
From: "C. Diekmann" <email@example.com>
<trolling>I don't think that Isabelle/HOL can prove that one graph is
isomorphic, but Isabelle/HOL may be able to prove that two graphs are
isomorphic or that any graph is isomorphic to itself.</trolling>
As an example, https://www.isa-afp.org/entries/Graph_Theory.html contains
one section labeled "Isomorphisms of Digraphs".
From: Jakub Kądziołka <firstname.lastname@example.org>
there is a formalization of some aspects of graph theory available here:
In particular, isomorphisms are defined for directed graphs in section
11 of the proof document (theory Digraph_Isomorphism). You can also use
it for undirected graphs by ensuring all edges are bidirectional.
From: Thomas Sewell <email@example.com>
Other people have given you some detailed/specific answers, but I think
that, since you found Isabelle by following libraries around, we should
clear up the general picture a bit. Isabelle is mostly a tool for
proofs that are well understood. If you think you have an argument or
why two graphs are isomorphic, Isabelle can help you check that.
If you're looking for some software to help you compute whether two
are isomorphic or not, I think you would be better off looking
I hope I'm not underestimating your understanding ;-)
Last updated: Sep 25 2021 at 08:21 UTC