### Abstract

Kleene algebras with domain are Kleene algebras endowed with an operation that maps each element of the algebra to its domain of definition (or its complement) in abstract fashion. They form a simple algebraic basis for Hoare logics, dynamic logics or predicate transformer semantics. We formalise a modular hierarchy of algebras with domain and antidomain (domain complement) operations in Isabelle/HOL that ranges from domain and antidomain semigroups to modal Kleene algebras and divergence Kleene algebras. We link these algebras with models of binary relations and program traces. We include some examples from modal logics, termination and program analysis.

### License

BSD License

### Topics

- Computer science/Programming languages/Logics
- Computer science/Automata and formal languages
- Mathematics/Algebra

### Session KAD

- Domain_Semiring
- Antidomain_Semiring
- Range_Semiring
- Modal_Kleene_Algebra
- Modal_Kleene_Algebra_Models
- Modal_Kleene_Algebra_Applications

### Depends on

- Kleene Algebra

### Used by

- Catoids, Categories, Groupoids
- Modal quantales, involutive quantales, Dedekind Quantales
- Verification Components for Hybrid Systems
- Program Construction and Verification Components Based on Kleene Algebra

### Auto-related entries

- Transport via Partial Galois Connections and Equivalences
- Transformer Semantics
- Program Construction and Verification Components Based on Kleene Algebra
- Binary Multirelations
- Relation Algebra

## Cite

×

KAD-AFP

    @article{KAD-AFP,
      author  = {Victor B. F. Gomes and Walter Guttmann and Peter Höfner and Georg Struth and Tjark Weber},
      title   = {Kleene Algebras with Domain},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/KAD.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
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Apr 12, 2016 : Isabelle2016