Our general interest is to understand the inherent complexity of contextual reasoning. In this paper we establish the bounded model property for propositional multi-context systems with finite sets of bridge rules: the number of local models needed to satisfy a set of formulas in such systems is bounded by the number of formulas in that set plus the number of bridge rules of the system. Using this result we achieve NP-completeness and a tractable encoding of contextual satisfiability into propositional satisfiability. In doing so, we pave the way for the implementation of contextual reasoners based on already existing specialized SAT solvers
Bounded Model Property for Multi-Context Systems
Roelofsen, Floris
2004-01-01
Abstract
Our general interest is to understand the inherent complexity of contextual reasoning. In this paper we establish the bounded model property for propositional multi-context systems with finite sets of bridge rules: the number of local models needed to satisfy a set of formulas in such systems is bounded by the number of formulas in that set plus the number of bridge rules of the system. Using this result we achieve NP-completeness and a tractable encoding of contextual satisfiability into propositional satisfiability. In doing so, we pave the way for the implementation of contextual reasoners based on already existing specialized SAT solversI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
