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 a state-of-the-art tableau-based system. In this paper we provide the theoretical foundations for developing SAT-based decision procedures for many different modal logics
From Tableau-based to SAT-based procedures - preliminary report
Sebastiani, Roberto;Giunchiglia, Fausto
1997
Abstract
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 a state-of-the-art tableau-based system. In this paper we provide the theoretical foundations for developing SAT-based decision procedures for many different modal logicsFile in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
