Boolean logics with relations (Q604451)

This paper contains, for the most part, a systematic study of Boolean logic with relations along the usual lines of modal logic. Based on Boolean terms, the formulas of the underlying language may assert equivalence of such terms as well as certain relational connections which are expressed with the aid of corresponding symbols. The common Boolean connectives are available in formulas, too. The authors provide two semantics of their language. The first one, called Kripke semantics, is inspired by region-based calculi for spatial reasoning, so that the relation expressions are interpreted as properties which should hold for some points of the regions the involved Boolean terms denote. For the second, called Boolean semantics, the Boolean variables denominate elements of a non-degenerate Boolean algbra, and the relation expressions are interpreted as usual in this case. In a section on correspondence, it is shown how the two semantics are related. Furthermore, several properties of Kripke and, respectively, Boolean structures are given and proved to be correspondents. This is followed by introducing an appropriate notion of bisimulation and proving the related Hennessy-Milner theorem. Adjusting the modal filtration technique suitably, the authors show that their logic is decidable. They also give a lower and an upper bound of the complexity of the associated satisfiability problem. Then, the question of axiomatizing their Boolean logic with relations is treated. A list of axiom schemata is provided and, among other things, proved to be sound and complete with respect to both semantics. Finally, two notions of canonicity of properties definable in the new language are introduced and shown to be different with an example.