Generalised Proof-Theory for Multi-Agent Autoepistemic Reasoning

First International Conference on Multiagent Systems

Volume

First International Conference on Multiagent Systems

Contents

Over the past few years, several different approaches have been proposed to deal with multi-agent autoepistemic reasoning. Despite some limitations, each approach is important in its own right. While Parikh’s approach allows an agent to reason nonmonotonically about other agents’ knowledge, it cannot reason about other agents’ nonmonotonic reasoning. Morgenstern’s logic provides a limited way to deal with the problem but unfortunately it is not constructive. Although Halpern introduces an algorithmic definition of multi-agent nonmonotonic reasoning, his approach cannot deal with default reasoning even for the single-agent case. The purpose of this paper is to propose an integrated theory that deals with these problems. Using examples from speech acts theory, we demonstrate some unintuitive results against existing approaches. We then develop a simple and yet generalised proof-theoretic framework with constructive interpretation for multi-agent autoepistemic reasoning. We show that this framework retains the advantages of existing approaches but does not have their peculiar results. Surprisingly, the new proof-theoretic framework can be obtained by a simple modification of Parikh’s approach. Furthermore, the results show that our framework generalises Morgenstern’s approach.