{"_id":"CTM87rc6Ws6NMf8nR","bibbaseid":"hustadt-schmidt-formulaewhichhighlightdifferencesbetweentemporallogicanddynamiclogicprovers-2001","author_short":["Hustadt, U.","Schmidt, R. A."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Hustadt"],"firstnames":["Ullrich"],"suffixes":[]},{"propositions":[],"lastnames":["Schmidt"],"firstnames":["Renate","A."],"suffixes":[]}],"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":[{"propositions":[],"lastnames":["Giunchiglia"],"firstnames":["E."],"suffixes":[]},{"propositions":[],"lastnames":["Massacci"],"firstnames":["F."],"suffixes":[]}],"publisher":"Dipartimento di Ingegneria dell'Informazione, Unversitá degli Studi di Siena","pages":"68-76","paddress":"Siena, Italy","pyear":"2001","caddress":"Siena, Italy","cyear":"2001","cmonth":"June 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.","bibtex":"@INPROCEEDINGS{Hustadt+Schmidt@IDEESMTL2001,\n AUTHOR = {Hustadt, Ullrich and Schmidt, Renate A.},\n TITLE = {Formulae which Highlight Differences between \n Temporal Logic and Dynamic Logic Provers},\n BOOKTITLE = {Issues in the Design and Experimental Evaluation of\n Systems for Modal and Temporal Logics},\n YEAR = {2001},\n EDITOR = {Giunchiglia, E. and Massacci, F.},\n PUBLISHER = {Dipartimento di Ingegneria dell'Informazione,\n Unversit{\\'a} degli Studi di Siena},\n PAGES = {68-76},\n PADDRESS = {Siena, Italy},\n PYEAR = {2001},\n CADDRESS = {Siena, Italy},\n CYEAR = {2001},\n CMONTH = jun # {~18--19},\n SERIES = {Technical Report DII 14/01},\n URL = {Hustadt+Schmidt@IDEESMTL2001.pdf},\n ABSTRACT = {In this Note we compare different inference methods for\n propositional temporal logic by empirical analysis.\n We define a class of randomly generated temporal logic formulae which\n we use to investigate the behaviour of a tableaux-based temporal logic approach\n using the Logics Workbench, a tableaux-based approach for propositional\n dynamic logic using an appropriate translation and the prover\n DLP, and temporal resolution using TRP.}\n}\n","author_short":["Hustadt, U.","Schmidt, R. A."],"editor_short":["Giunchiglia, E.","Massacci, F."],"key":"Hustadt+Schmidt@IDEESMTL2001","id":"Hustadt+Schmidt@IDEESMTL2001","bibbaseid":"hustadt-schmidt-formulaewhichhighlightdifferencesbetweentemporallogicanddynamiclogicprovers-2001","role":"author","urls":{"Paper":"http://cgi.csc.liv.ac.uk/~ullrich/publications/Hustadt+Schmidt@IDEESMTL2001.pdf"},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"http://cgi.csc.liv.ac.uk/~ullrich/publications/all.bib?authorFirst=1","dataSources":["WhiGijHmCtTSdLaAj","FgmYE34DdKWThg2dR"],"keywords":[],"search_terms":["formulae","highlight","differences","between","temporal","logic","dynamic","logic","provers","hustadt","schmidt"],"title":"Formulae which Highlight Differences between Temporal Logic and Dynamic Logic Provers","year":2001}