Re: [isabelle] How to formalize a large digraph in Isabelle?



Hi Scott,


>> I mean any other kind of digraph, e.g. the graph of all sets as vertices

>> and all functions as directed edges. How can this be formalized in
>> Isabelle? Or do limitations of HOL preclude such a formalization?


Indeed, such things cannot be represented in HOL. But you could use extensions of HOL, such as Steven Obua's HOLZF:


http://isabelle.in.tum.de/library/HOL/HOL-ZF/HOLZF.html


(see also section 3 in https://mediatum.ub.tum.de/doc/1094432/1094432.pdf)


Best,

  Andrei





________________________________
From: cl-isabelle-users-bounces at lists.cam.ac.uk <cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of scott constable <sdconsta at syr.edu>
Sent: 02 November 2016 16:25
To: isabelle-users at cl.cam.ac.uk
Subject: [isabelle] How to formalize a large digraph in Isabelle?

Hi All,

The paper
https://www21.in.tum.de/~noschinl/documents/noschinski2013graphs.pdf gives
a reasonable method for formalizing small digraphs is Isabelle. By "small"
I mean a digraph which has sets of vertices and directed edges. By "large"
I mean any other kind of digraph, e.g. the graph of all sets as vertices
and all functions as directed edges. How can this be formalized in
Isabelle? Or do limitations of HOL preclude such a formalization?

Scott Constable



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