Analytic cut-free Tableaux for regular modal logics of agent beliefs

Abstract

We present a sound and complete tableau calculus for a class 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 . We demonstrate the usefulness of logics and our tableau calculus using the wise men puzzle and its modified version, which requires axiom (5) for single agents. Show more