Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Relational Forests

view this post on Zulip Email Gateway (Aug 08 2021 at 09:07):

From: Tobias Nipkow <>
Relational Forests
Walter Guttmann

We study second-order formalisations of graph properties expressed as
first-order formulas in relation algebras extended with a Kleene star. The
formulas quantify over relations while still avoiding quantification over
elements of the base set. We formalise the property of undirected graphs being
acyclic this way. This involves a study of various kinds of orientation of
graphs. We also verify basic algorithms to constructively prove several
second-order properties.


Last updated: Dec 08 2021 at 08:24 UTC