Stream: Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 08 2021 at 09:07):

From: Tobias Nipkow <nipkow@in.tum.de>
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.

https://www.isa-afp.org/entries/Relational_Forests.html

Enjoy!
smime.p7s

Last updated: Apr 19 2024 at 01:05 UTC