Anytime Approximate Modal Reasoning

Propositional modal logics have two independent sources of complexity: unbounded logical omniscience and unbounded logical introspection. This paper discusses an approximation method to tame both of them, by merging propositional approximations with a new technique tailored for multi-modal logics. It provides both skeptical and credulous approximations (or approximation that are neither of the two). On this semantics we build an anytime proof procedure with a simple modification to classical modal tableaux. The procedure yields approximate proofs whose precision increases as we have more resources (time, space etc.) and we analyze its semantical and computational `quality guarantees'.