Formulae which Highlight Differences between Temporal Logic and Dynamic Logic Provers

Hustadt, U. and Schmidt, R. A. (2001)

In Giunchiglia, E. and Massacci, F. (eds), Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics. Technical Report DII 14/01, Dipartimento di Ingegneria dell'Informazione, Unversitä degli Studi di Siena, Siena, Italy, 68-76. 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.


Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 31 Jan 2002
Copyright © 2001,2 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk