Tableaux and Complexity Bounds for a Multiagent Justification Logic with Interacting Justifications

摘要

We introduce a family of multi-agent justification logics with interactions between the agents' justifications, by extending and generalizing the two-agent versions of the Logic of Proofs (LP) introduced by Yavorskaya in 2008. LP, and its successor, Justification Logic, is a refinement of the modal logic approach to epistemology in which for every belief assertion, an explicit justification is supplied. This affects the complexity of the logic's derivability problem, which is known to be in the second level of the polynomial hierarchy (first result by Kuznets in 2000) for all single-agent justification logics whose complexity is known. We present tableau rules and some complexity results. In several cases the satisfiability problem for these logics remains in the second level of the polynomial hierarchy, while the problem becomes PSPACE-hard for certain two-agent logics and there are EXP-hard logics of three agents.