---
title: "On Evaluating Decision Procedures for Modal Logic"
authors:
  - "Ullrich Hustadt"
  - "Renate A. Schmidt"
doi: ""
url: "https://ijcai.org/proceedings/1997/31"
pdf: "https://ijcai.org/proceedings/1997/0031.pdf"
venue: "Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence"
year: 1997
pages: "202-208"
track: "Automated Reasoning"
keywords:
---

# On Evaluating Decision Procedures for Modal Logic

Ullrich Hustadt, Renate A. Schmidt

*Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence*, 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 .