Formulae which Highlight Differences between Temporal Logic and Dynamic Logic Provers. Hustadt, U. & Schmidt, R. A. In Giunchiglia, E. & Massacci, F., editors, Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics, of Technical Report DII 14/01, pages 68-76, 2001. Dipartimento di Ingegneria dell'Informazione, Unversitá degli Studi di Siena.
Formulae which Highlight Differences between Temporal Logic and Dynamic Logic Provers [pdf]Paper  abstract   bibtex   
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.
@INPROCEEDINGS{Hustadt+Schmidt@IDEESMTL2001,
 AUTHOR        = {Hustadt, Ullrich and Schmidt, Renate A.},
 TITLE         = {Formulae which Highlight Differences between 
 Temporal Logic and Dynamic Logic Provers},
 BOOKTITLE     = {Issues in the Design and Experimental Evaluation of
 Systems for Modal and Temporal Logics},
 YEAR          = {2001},
 EDITOR        = {Giunchiglia, E. and Massacci, F.},
 PUBLISHER     = {Dipartimento di Ingegneria dell'Informazione,
 Unversit{\'a} degli Studi di Siena},
 PAGES         = {68-76},
 PADDRESS      = {Siena, Italy},
 PYEAR         = {2001},
 CADDRESS      = {Siena, Italy},
 CYEAR         = {2001},
 CMONTH        = jun # {~18--19},
 SERIES        = {Technical Report DII 14/01},
 URL           = {Hustadt+Schmidt@IDEESMTL2001.pdf},
 ABSTRACT      = {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.}
}
Downloads: 0