SAT-based decision procedures for normal modal logics: a theoretical framework

Tableau systems are very popular in AI for their simplicity and versatility. In recent papers we showed that tableau-based procedures are intrinsically inefficient, and proposed an alternative approach of building decision procedures on top of SAT decision procedure. We called this approach `SAT-based`. In extensive empirical tests on the case study of modal K, a SAT-based procedure drastically outperformed state-of-the-art tableau-based systems. In this paper we provide the theoretical foundations for developing SAT-based decision procedures for many different modal logics