Kleene Algebras with Domain (Q7361028)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry KAD
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Kleene Algebras with Domain |
AFP entry KAD |
Statements
12 April 2016
0 references
Victor B. F. Gomes
0 references
Walter Guttmann
0 references
Peter Höfner
0 references
Georg Struth
0 references
Tjark Weber
0 references
Kleene Algebras with Domain (English)
0 references
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.
0 references
