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