On Evaluating Decision Procedures for Modal Logic

This paper investigates the evaluation method of decision procedures for multi-modal logic proposed by Giunchiglia and Sebastiani as an adaptation from the evaluation method of Mitchell et al of decision procedures for propositional logic. We compare three dif­ ferent theorem proving approaches, namely the Davis-Putnam-based procedure KSAT, the tableaux-based system KTUS and a transla­ tion approach combined with first-order resolu­ tion. Our results do not support the claims of Giunchiglia and Sebastiani concerning the com­ putational superiority of KSAT over KRIS, and an easy-hard-easy pattern for randomly gener­ ated modal formulae.

• Type: Conference
• Year: 1997
• Where: IJCAI
• Authors: Ullrich Hustadt, Renate A. Schmidt
• Keywords: Decision Procedures, Evaluation Method, First-order Resolu­ Tion, IJCAI 1997, IJCAI 2007