Distributed Nonmonotonic Multi-Context Systems

We present a distributed algorithm for computing equilibria of heterogeneous nonmonotonic multi-context systems (MCS). The algorithm can be parametrized to compute only partial equilibria, which can be used for reasoning tasks like query answering or satisfiability checking that need only partial information and not whole belief states. Furthermore, caching is employed to cut redundant solver calls. As a showcase, we instantiate the MCS framework with answer set program contexts. To characterize equilibria of such MCS, we develop notions of loop formulas that enable reductions to the classical satisfiability problem (SAT). Notably, loop formulas for bridge rules between contexts and for the local contexts can be combined to a uniform encoding of an MCS into a (distributed) SAT instance. As a consequence, we can use SAT solvers for belief set building. We demonstrate this approach by an experimental prototype implementation, which uses an off-the-shelf SAT solver.

• Type: Conference
• Year: 2010
• Where: KR
• Authors: Minh Dao-Tran, Thomas Eiter, Michael Fink, Thomas Krennwallner
• Keywords: Automated Reasoning, KR 2010, Loop Formulas, Nonmonotonic Multi-context Systems, Sat Solver