Finite Representations in Relation Algebra

Binary relations provide a great abstraction for a number of concepts, both in theoretical and applied topics. This is why structures of binary relations have found applications in formal verification, temporal and spatial reasoning in AI, regular language equivalence, sequent calculi, and more. In general, a finite relation algebra cannot be finitely represented. This negatively impacts the feasibility of implementing any of the aforementioned applications based on these structures. Our work focuses on finding large classes of relational structures for which the finite representation property either holds or fails. Furthermore, we examine related topics such as the decidability of the [finite] representation problem and finite axiomatisability. Moreover, we examine the relationship between these properties. We refine Hirsch’s conjecture on which relation algebra reduct signatures have the finite representation property and prove the negative implication of it. Furthermore, we provide a number of results that reveal a possible direction for proving the positive side. We present the first known signature that fails to have a finitely axiomatisable representation class but has the finite representation property. We generalise the results for the undecidability of the representation decision problem and show that semigroups with the Heyting implication fail to have the said problem decidable. We prove and disprove a number of properties for the structures of binary relations with combined operators, motivated by various topics in computer science. Finally, we show a number of results in the area of weakening relation algebras and show the finite weakening representation property for some signatures with their finite representation property open.