On Evaluating Decision Procedures for Modal Logic
Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence. Automated Reasoning. Pages 202-208.
Abstract
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 different theorem proving approaches, namely, the Davis-Putnam-based procedure KSAT, the tableaux-based system ICRIS and a translation approach combined with first-order resolution. Our results do not support the claims of Giunchiglia and Sebastiani concerning the computational superiority of KsAT over ICRIS, and an easy-hard-easy pattern for randomly generated modal formulae .
@inproceedings{ijcai1997p31,
title = {On Evaluating Decision Procedures for Modal Logic},
author = {Hustadt, Ullrich and Schmidt, Renate A.},
booktitle = {Proceedings of the Fifteenth International Joint Conference on
Artificial Intelligence, {IJCAI-97}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Martha E. Pollack},
pages = {202--208},
year = {1997},
note = {Automated Reasoning},
url = {https://ijcai.org/proceedings/1997/31},
}
TY - CPAPER TI - On Evaluating Decision Procedures for Modal Logic AU - Hustadt, Ullrich AU - Schmidt, Renate A. T2 - Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence, IJCAI-97 PB - International Joint Conferences on Artificial Intelligence PY - 1997 SP - 202 EP - 208 UR - https://ijcai.org/proceedings/1997/31 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
