Re: [isabelle] First day with HOL/Isabelle



On Sat Feb 20, 2021 at 6:24 PM CET, McCue, Brian wrote:
> Can HOL/Isabelle be used with graph theory to prove whether a graph is isomorphic?

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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.