A Tableau Calculus for a Multi-modal Logic of Dishonesty

Abstract

In recent years, several approaches for formalising dishonest agents have been proposed in the artificial-intelligence literature. In particular, many of these approaches are based on a modal-logic setting. A prominent specimen of such a formalism is the multi-modal logic BIC, proposed by Sakama, Caminada, and Herzig, where the name "BIC" stands for belief, intention, and communication. In their work, Sakama et al. introduce a Kripke semantics for BIC and provide a corresponding Hilbert-style axiomatisation. In this paper, we complement this investigation by introducing a tableau calculus for BIC. Our approach is based on the single-step tableau method, an important proof method for automated deduction, originally proposed by Massacci for certain normal modal logics and subsequently elaborated by Goré. We provide soundness and completeness proofs, extending methods of Goré.