*To*: brian.mccue at snhu.edu*Subject*: Re: [isabelle] First day with HOL/Isabelle*From*: "C. Diekmann" <diekmann at in.tum.de>*Date*: Sun, 21 Feb 2021 16:49:16 +0100*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <BN3PR05MB2658C4F421382C79D03FA78085839@BN3PR05MB2658.namprd05.prod.outlook.com>*References*: <BN3PR05MB2658C4F421382C79D03FA78085839@BN3PR05MB2658.namprd05.prod.outlook.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".

HTH

Cornelius

Am Sa., 20. Feb. 2021 um 18:24 Uhr schrieb McCue, Brian <brian.mccue at 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.

**References**:**[isabelle] First day with HOL/Isabelle***From:*McCue, Brian

- Previous by Date: Re: [isabelle] Predicate Compiler fails with "No specification for ..."
- Next by Date: Re: [isabelle] Predicate Compiler fails with "No specification for ..."
- Previous by Thread: [isabelle] First day with HOL/Isabelle
- Next by Thread: Re: [isabelle] First day with HOL/Isabelle
- Cl-isabelle-users February 2021 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list