### Abstract

Binary relations are one of the standard ways to encode, characterise and reason about graphs. Relation algebras provide equational axioms for a large fragment of the calculus of binary relations. Although relations are standard tools in many areas of mathematics and computing, researchers usually fall back to point-wise reasoning when it comes to arguments about paths in a graph. We present a purely algebraic way to specify different kinds of paths in Kleene relation algebras, which are relation algebras equipped with an operation for reflexive transitive closure. We study the relationship between paths with a designated root vertex and paths without such a vertex. Since we stay in first-order logic this development helps with mechanising proofs. To demonstrate the applicability of the algebraic framework we verify the correctness of three basic graph algorithms.

### License

BSD License

### Topics

- Mathematics/Graph theory

### Session Relational_Paths

- More_Relation_Algebra
- Paths
- Rooted_Paths
- Path_Algorithms

### Depends on

- Relation Algebra

### Auto-related entries

- A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
- Soundness and Completeness of an Axiomatic System for First-Order Logic
- A Sequent Calculus for First-Order Logic
- Abstract Soundness
- First-Order Logic According to Fitting

## Cite

×

Relational_Paths-AFP

    @article{Relational_Paths-AFP,
      author  = {Walter Guttmann and Peter Höfner},
      title   = {Relational Characterisations of Paths},
      journal = {Archive of Formal Proofs},
      month   = {July},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/Relational_Paths.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
- Feb 23, 2021 : Isabelle2021
- Jul 28, 2020 : Isabelle2020