Hirsch, R;
(2018)
Decidability of equational theories for subsignatures of relation algebra.
In:
Relational and Algebraic Methods in Computer Science. RAMiCS 2018. Lecture Notes in Computer Science, vol 11194.
(pp. pp. 87-96).
Springer: Cham.
Preview |
Text
Hirsch_ramics.pdf - Accepted Version Download (326kB) | Preview |
Abstract
Let S be a subset of the signature of relation algebra. Let R(S) be the closure under isomorphism of the class of proper S-structures and let F(S) be the closure under isomorphism of the class of proper S-structures over finite bases. Based on previous work, we prove that membership of R(S) is undecidable when (Formula presented), and for any of these signatures S if converse is excluded from S then membership of F(S) is also undecidable, for finite S-structures. We prove that the equational theories of F(S) and R(S) are undecidable when S includes composition and the signature of boolean algebra. If all operators in S are positive and it does not include negation, or if it can define neither domain, range nor composition, then the equational theory of either class is decidable. Open cases for decidability of the equational theory of R(S) are when S can define negation but not meet (or join) and either domain, range or composition. Open cases for the decidability of the equational theory of F(S) are (i) when S can define negation, converse and either domain, range or composition, and (ii) when S contains negation but not meet (or join) and either domain, range or composition.
Type: | Proceedings paper |
---|---|
Title: | Decidability of equational theories for subsignatures of relation algebra |
Event: | Relational and Algebraic Methods in Computer Science. RAMiCS 2018 |
ISBN-13: | 9783030021481 |
Open access status: | An open access version is available from UCL Discovery |
DOI: | 10.1007/978-3-030-02149-8_6 |
Publisher version: | https://doi.org/10.1007/978-3-030-02149-8_6 |
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: | Equational Theory, Relational Algebra, Subsignature, Finite Basis, Quantifier-free Theory |
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/10062931 |




Archive Staff Only
![]() |
View Item |