More Evaluation of Decision Procedures for Modal Logics.
Enrico Giunchiglia, Fausto Giunchiglia, Roberto Sebastiani, Armando Tacchella · 1998
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 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 Ohlbach's translation method. Our results contradict some of the results presented in previous papers.