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”.

Authors

• Fabio Massacci

Keywords

No keywords are indexed for this paper.