Theorem-Proving for Modal Logics

Cláudia Nalon, University of Brasília. Part of the algebra, logic, and algorithms seminar series.

Modal logics have been extensively used for representing and reasoning about complex computational systems.  The reasoning tasks for these logics are, however, far from trivial: the local and global satisfiability problems for the basic multimodal propositional logic K are PSPACE-complete and EXPTime-complete, respectively.  Given the inherent intractability of the reasoning problems and also the wide range of applications to which those logics can be applied, the development of automatic, efficient tools for theorem proving is highly desirable.  In this talk, we will discuss some successful strategies for classical theorem-proving and how they can be adapted for the modal case.  We will also report on successful techniques for a resolution-based calculus we have recently developed and implemented for those logics.