Hirsch, R;
Stokes, T;
(2021)
Axioms for signatures with domain and demonic composition.
Algebra universalis
, 82
(2)
, Article 24. 10.1007/s00012-021-00719-4.
Preview |
Text
demonic-revised-post-review.pdf - Accepted Version Download (346kB) | Preview |
Abstract
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 {⊆,∘,∗}.
| Type: | Article |
|---|---|
| Title: | Axioms for signatures with domain and demonic composition |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/s00012-021-00719-4 |
| Publisher version: | https://doi.org/10.1007/s00012-021-00719-4 |
| Language: | English |
| Additional information: | This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. |
| Keywords: | Demonic composition, demonic refinement, binary relation, non-deterministic program, total correctness, axiomatisation. |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10134566 |
Loading...
Loading...Loading...Loading...Archive Staff Only
 |
View Item |
