Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] First day with HOL/Isabelle


view this post on Zulip Email Gateway (Feb 21 2021 at 11:05):

From: "McCue, Brian" <brian.mccue@snhu.edu>
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.

view this post on Zulip Email Gateway (Feb 21 2021 at 15:49):

From: "C. Diekmann" <diekmann@in.tum.de>
<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".

HTH
Cornelius

view this post on Zulip Email Gateway (Feb 21 2021 at 18:29):

From: Jakub Kądziołka <kuba@kadziolka.net>
Brian,

there is a formalization of some aspects of graph theory available here:

https://www.isa-afp.org/entries/Graph_Theory.html

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.

Regards,
Jakub Kądziołka

view this post on Zulip Email Gateway (Feb 21 2021 at 20:04):

From: Thomas Sewell <tals4@cam.ac.uk>
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
checking
proofs that are well understood. If you think you have an argument or
proof
why two graphs are isomorphic, Isabelle can help you check that.

If you're looking for some software to help you compute whether two
concrete graphs
are isomorphic or not, I think you would be better off looking
elsewhere.

I hope I'm not underestimating your understanding ;-)

Cheers,
Thomas.


Last updated: Mar 28 2024 at 12:29 UTC