zbMATH — the first resource for mathematics

SAT-based decision procedures for normal modal logics: A theoretical framework. (English) Zbl 0927.03029
Giunchiglia, Fausto (ed.), Artificial intelligence: methodology, systems, and applications. 8th international conference, AIMSA ’98. Sozopol, Bulgaria, September 21–23, 1998. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1480, 377-388 (1998).
Summary: 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.
For the entire collection see [Zbl 0903.00073].
03B35 Mechanization of proofs and logical operations
03B45 Modal logic (including the logic of norms)