Relation-changing modal logics: some model and proof theoretic aspects

We can fairly say that Logic (whichever you want to choose, be it propositional or first-order, classical or non-classical) is the mathematical tool used, par excellence, to describe a structure. Modal logics, for example, are particularly well suited to describe relational structures, specially if one is interested in computationally well behaved formalisms. But why can a logic only describe a structure? In this talk we introduce relation-changing modal logics, a family of modal logics that can change the accessibility relation of a model during the evaluation of a formula. We consider some model and proof theoretic aspects of relation-changing modal logics. We start by illustrating some inexpressible properties such as the tree and finite model properties, and we show that these logics can be seen as fragments of hybrid logics by providing satisfiability-preserving translations. Then, we present sound and complete tableau methods using hybrid logic tools, and we conclude with some open questions aiming at integrating relation-changing modal logics within the current landscape of logics of model update.