Anytime Approximate Modal Reasoning

Fabio Massacci

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

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.