Complexity of Contextual Reasoning

The aim of this paper is to delineate the computational complexity of propositional multi-context systems. We establish NP-completeness by translating multi-context systems into bounded modal, and obtain more refined complexity results by achieving the so-called bounded model property: the number of local models needed to satisfy a set of formulas in a multi-context system is bounded by the number of formulas in that set plus the number of bridge rules of the system. Exploiting this property of multi-context systems, we are able to encode contextual satisfiability problems into propositional ones, providing for the implementation of contextual reasoners based on specialized Sat solvers. We apply our results to improve on complexity bounds for Mc-Carthy's propositional logic of context - we show that satisfiability in this framework can be settled in non-deterministic polynomial time.