This paper follows on previous papers which present and evaluate various decision procedures for modal logics. It confirms previous experimental results in showing that SAT based decision procedures, i.e., the procedures built on top of decision procedures for propositional satisfiability, are more efficient than tableau based decision procedures. It also confirms previous evidence of an easy-hard-easy pattern in the satisfiability curve for modal K. Finally, it provides further experimental results, suggesting that SAT based decision procedures are also more efficient than the decision procedures based on translation methods. These results contradict some of the claims presented in previous papers by other authors
SAT vs. Translation Based decision procedures for modal logics: a comparative evaluation
Giunchiglia, Fausto;Sebastiani, Roberto;
2000-01-01
Abstract
This paper follows on previous papers which present and evaluate various decision procedures for modal logics. It confirms previous experimental results in showing that SAT based decision procedures, i.e., the procedures built on top of decision procedures for propositional satisfiability, are more efficient than tableau based decision procedures. It also confirms previous evidence of an easy-hard-easy pattern in the satisfiability curve for modal K. Finally, it provides further experimental results, suggesting that SAT based decision procedures are also more efficient than the decision procedures based on translation methods. These results contradict some of the claims presented in previous papers by other authorsI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
