This paper follows on previous papers which presented and evaluated 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 far 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 far more efficient that the decision procedures based on Ohlbach's translation method. Our results contradict some of the results presented in previous papers
More Evaluation of Decision Procedures for Modal Logics
Giunchiglia, Fausto;Sebastiani, Roberto;
1998-01-01
Abstract
This paper follows on previous papers which presented and evaluated 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 far 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 far more efficient that the decision procedures based on Ohlbach's translation method. Our results contradict some of the results presented in previous papersI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
