U. Hustadt, and R. A. Schmidt (2001): Formulae which Highlight Differences between Temporal Logic and Dynamic Logic Provers

U. Hustadt, R. A. Schmidt (2001): ``Formulae which Highlight Differences between Temporal Logic and Dynamic Logic Provers.'' In E. Giunchiglia and F. Massacci, editors, Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics, pp. 68-76. Technical Report DII 14/01, Dipartimento di Ingegneria dell'Informazione, Unversitá degli Studi di Siena, 2001.
Abstract, BibTeX, PostScript.

In this Note we compare different inference methods for propositional temporal logic by empirical analysis. We define a class of randomly generated temporal logic formulae which we use to investigate the behaviour of a tableaux-based temporal logic approach using the Logics Workbench, a tableaux-based approach for propositional dynamic logic using an appropriate translation and the prover DLP, and temporal resolution using TRP. [an error occurred while processing this directive]