### 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.

### License

BSD License

### Topics

- Mathematics/Graph theory

### Session Relational_Forests

- Forests
- Algorithms

### Depends on

- Stone-Kleene Relation Algebras

## Cite

×

Relational_Forests-AFP

    @article{Relational_Forests-AFP,
      author  = {Walter Guttmann},
      title   = {Relational Forests},
      journal = {Archive of Formal Proofs},
      month   = {August},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Relational_Forests.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Aug 8, 2021 : Isabelle2021