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 $K_n$, 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 McCarthy`s propositional logic of context we show that satisfiability in this framework can be settled in non-deterministic polynomial time O(|phi|^2)
Complexity of Contextual Reasoning
Serafini, Luciano;Roelofsen, Floris
2004-01-01
Abstract
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 $K_n$, 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 McCarthy`s propositional logic of context we show that satisfiability in this framework can be settled in non-deterministic polynomial time O(|phi|^2)I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
