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.
  author  = {Walter Guttmann},
  title   = {Relational Forests},
  journal = {Archive of Formal Proofs},
  month   = aug,
  year    = 2021,
  note    = {\url{},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Depends on: Stone_Kleene_Relation_Algebras
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.