This paper, we propose a modal logic satisfying minimal requirements for reasoning about diagrams via collection of sets and relations between them, following Harel's proposal. We first give an axiomatics of such a theory and then provide its Kripke semantics. Then we extend previous works of ours in order to obtain a decision procedure based on tableaux for this logic. Beside soundness and completeness of our tableaux, we manage to define a strategy of rule application ensuring termination by extending the (...) usual loop test of modal logic S4 to whole sub-structures of the model being computed. (shrink)

The problem of completeness for predicate modal logics is still under investigation, although some results have been obtained in the last few years . As far as we know, the case of multimodal logics has not been addressed at all. In this paper, we study the combination of modal logics in terms of combining their semantics. We demonstrate by a simple example that in this sense predicate modal logics are not so easily manipulated as propositional ones: mixing two Kripke-complete predicate (...) modal logics results in a Kripke-incomplete system. (shrink)