# Relational Forests

 Title: Relational Forests Author: Walter Guttmann Submission date: 2021-08-03 Abstract: 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. BibTeX: @article{Relational_Forests-AFP, author = {Walter Guttmann}, title = {Relational Forests}, journal = {Archive of Formal Proofs}, month = aug, year = 2021, note = {\url{https://isa-afp.org/entries/Relational_Forests.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: Stone_Kleene_Relation_Algebras