PSpace reasoning for graded modal logics (Q2720401)

The paper presents a PSpace algorithm that decides satisfiability of graded modal logic \(\text{Gr(K}_R)\) -- a natural extension of the propositional modal logic \(\text{K}_R\) by counting expressions. The algorithm is based on the tableaux algorithms for \(\text{K}_R\) and tries to prove satisfiability of a given formula by explicitly constructing a model for it. Using an extension of the proposed techniques, the author obtains a PSpace algorithm for the logic which extends \(\text{Gr(K}_R)\) by the inverse relation and the intersection of relations. This solves an open problem.