TY  - JOUR
EP  - 19
AV  - public
Y1  - 2021/05//
VL  - 82
TI  - Axioms for signatures with domain and demonic composition
N1  - This version is the author accepted manuscript. For information on re-use, please refer to the publisher?s terms and conditions.
IS  - 2
UR  - https://doi.org/10.1007/s00012-021-00719-4
PB  - SPRINGER BASEL AG
ID  - discovery10134566
N2  - Demonic composition ? is an associative operation on binary relations, and demonic refinement ? is a partial order on binary relations. Other operations on binary relations considered here include the unary domain operation D and the left restrictive multiplication operation ? given by s?t=D(s)?t. We show that the class of relation algebras of signature {?,D,?}, or equivalently {?,?,?}, has no finite axiomatisation. A large number of other non-finite axiomatisability consequences of this result are also given, along with some further negative results for related signatures. On the positive side, a finite set of axioms is obtained for relation algebras with signature {?,?,?}, hence also for {?,?,?}.
KW  - Demonic composition
KW  -  demonic refinement
KW  -  binary relation
KW  -  non-deterministic program
KW  -  total correctness
KW  -  axiomatisation.
A1  - Hirsch, R
A1  - Stokes, T
JF  - Algebra universalis
ER  -