Complexity of some modal logics of density (extended version)

TL;DR

This paper analyzes the computational complexity of certain modal logics of density, establishing EXPTIME and PSPACE bounds for their satisfiability problems using filtration and tableau methods.

Contribution

It introduces new complexity bounds for modal logics of density, employing novel proof techniques like selective filtration and tableau approaches.

Findings

Satisfiability of unimodal density logic is in EXPTIME.

Satisfiability of bimodal weak density logic is in PSPACE.

New proof methods improve understanding of modal logic complexity.

Abstract

By using a selective filtration argument, we prove that the satisfiability problem of the unimodal logic of density is in $EXPTIME$. By using a tableau-like approach, we prove that the satisfiability problem of the bimodal logic of weak density is in $PSPACE$.