A Representation Theorem for Reasoning in First-Order Multi-Agent Knowledge Bases
Christoph Schwering, Maurice Pagnucco · 2019
Levesque's notion of only-knowing provides a natural formalisation of a knowledge base: it precisely captures the beliefs and non-beliefs that follow from the knowledge base, including introspection and de dicto versus de re distinctions in a first-order setting. Apart from its attractive properties in terms of specification, a major result about only-knowing is Levesque's representation theorem, which shows how reasoning in (single-agent) knowledge bases can be Turing-reduced to ordinary first-order logic. While numerous proposals have been made to lift the logic of only-knowing to the multi-agent case, generalising the representation theorem has remained an open problem. In this paper, we develop a Turing reduction from reasoning in multi-agent knowledge bases to ordinary, non-epistemic first-order logic and thus obtain a new representation theorem for the multi-agent case.