Stream: Archive Mirror: Isabelle Users Mailing List

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

view this post on Zulip Email Gateway (Aug 22 2022 at 14:25):

From: scott constable <sdconsta@syr.edu>
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

view this post on Zulip Email Gateway (Aug 22 2022 at 14:30):

From: Andrei Popescu <A.Popescu@mdx.ac.uk>
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

Last updated: May 01 2024 at 20:18 UTC