Analytic Cut-Free Tableaux for Regular Modal Logics of Agent Beliefs

We present a sound and complete tableau calculus for a class BReg of extended regular modal logics which contains useful epistemic logics for reasoning about agent beliefs. Our calculus is cut-free and has the analytic superformula property so it gives a decision procedure. Applying sound global caching to the calculus, we obtain the first optimal (EXPTime) tableau decision procedure for BReg. We demonstrate the usefulness of BReg logics and our tableau calculus using the wise men puzzle and its modified version, which requires axiom (5) for single agents.

• Type: Conference
• Year: 2007
• Where: CLIMA
• Authors: Rajeev Goré, Linh Anh Nguyen
• Keywords: CLIMA 2007, Complete Tableau Calculus, Intelligent Agents, Tableau Calculus, Tableau Decision Procedure