CINECA IRIS Institutional Research Information System
IRIS è l’archivio della produzione scientifica della Fondazione Bruno Kessler.
EnglishTableau 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
Scheda prodotto non validato
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte di FBK.
| Titolo: | From Tableau-based to SAT-based procedures - preliminary report | |
| Autori: | ||
| Data di pubblicazione: | 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 logics | |
| Handle: | http://hdl.handle.net/11582/1470 | |
| Appare nelle tipologie: | 5.12 Altro |
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Utilizza questo identificativo per citare o creare un link a questo documento:
http://hdl.handle.net/11582/1470
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
Copyright © 2021