@INPROCEEDINGS{Hustadt+Schmidt@PAAR2010,
 AUTHOR        = {Hustadt, Ullrich and Schmidt, Renate, A.},
 TITLE         = {A Comparison of Solvers for Propositional Dynamic Logic},
 BOOKTITLE     = {Proceedings of the Workshop on Practical Aspect of Automated Reasoning (PAAR-2010)
 [Edinburgh, Scotland, 14 July 2010]},
 YEAR          = {2010},
 EDITOR        = {Konev, B. and Schmidt, Renate A. and Schulz, Stephan},
 PAGES         = {},
 CADDRESS      = {Edinburgh, Scotland},
 CYEAR         = {2010},
 CMONTH        = jul # {~14},
 URL           = {Hustadt+Schmidt@PAAR2010.pdf},
 ABSTRACT      = {Calculi for propositional dynamic logics have been investigated since
the introduction of this logic in the late seventies. Only in recent
years have practical procedures been suggested and implemented. In
this paper, we compare three such systems, namely, the
Tableau Workbench by Abate, Goré, and Widmann
(2009), the pdlProver system by Goré and Widmann (2009), and
the MLSolver system by Friedmann and Lange (2009).
<p>
The benchmarking formulae used in this paper are available in
MLSolver and pdlProver syntax:
<ul style="margin-top: -10; margin-left: 0; padding-left: 20px;">
<li>C<sub>PDL</sub><sup>1</sup> (n=5, k=3, p=0.5): 
in <a href="http://www.csc.liv.ac.uk/~ullrich/samples/paar2010/mlsolver-Cpdl1-5-3.zip">MLSolver syntax</a>, 
in <a href="http://www.csc.liv.ac.uk/~ullrich/samples/paar2010/pdlProver-Cpdl1-5-3.zip">pdlProver syntax</a>
</li>
<li>C<sub>PDL</sub><sup>2</sup> (n=5, k=3, p=0.5): 
in <a href="http://www.csc.liv.ac.uk/~ullrich/samples/paar2010/mlsolver-Cpdl2-5-3.zip">MLSolver syntax</a>, 
in <a href="http://www.csc.liv.ac.uk/~ullrich/samples/paar2010/pdlProver-Cpdl2-5-3.zip">pdlProver syntax</a>
</li>
</ul>}
}

{"_id":"LeNbDM2cREYa4pFcx","bibbaseid":"hustadt-schmidt-acomparisonofsolversforpropositionaldynamiclogic-2010","author_short":["Hustadt, U.","Schmidt, R."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Hustadt"],"firstnames":["Ullrich"],"suffixes":[]},{"propositions":[],"lastnames":["Schmidt"],"firstnames":["Renate"],"suffixes":["A."]}],"title":"A Comparison of Solvers for Propositional Dynamic Logic","booktitle":"Proceedings of the Workshop on Practical Aspect of Automated Reasoning (PAAR-2010) [Edinburgh, Scotland, 14 July 2010]","year":"2010","editor":[{"propositions":[],"lastnames":["Konev"],"firstnames":["B."],"suffixes":[]},{"propositions":[],"lastnames":["Schmidt"],"firstnames":["Renate","A."],"suffixes":[]},{"propositions":[],"lastnames":["Schulz"],"firstnames":["Stephan"],"suffixes":[]}],"pages":"","caddress":"Edinburgh, Scotland","cyear":"2010","cmonth":"July 14","url":"Hustadt+Schmidt@PAAR2010.pdf","abstract":"Calculi for propositional dynamic logics have been investigated since the introduction of this logic in the late seventies. Only in recent years have practical procedures been suggested and implemented. In this paper, we compare three such systems, namely, the Tableau Workbench by Abate, Gor&eacute;, and Widmann (2009), the pdlProver system by Gor&eacute; and Widmann (2009), and the MLSolver system by Friedmann and Lange (2009). <p> The benchmarking formulae used in this paper are available in MLSolver and pdlProver syntax: <ul style=\"margin-top: -10; margin-left: 0; padding-left: 20px;\"> <li>C_PDL¹ (n=5, k=3, p=0.5): in <a href=\"http://www.csc.liv.ac.uk/ ullrich/samples/paar2010/mlsolver-Cpdl1-5-3.zip\">MLSolver syntax</a>, in <a href=\"http://www.csc.liv.ac.uk/ ullrich/samples/paar2010/pdlProver-Cpdl1-5-3.zip\">pdlProver syntax</a> </li> <li>C_PDL² (n=5, k=3, p=0.5): in <a href=\"http://www.csc.liv.ac.uk/ ullrich/samples/paar2010/mlsolver-Cpdl2-5-3.zip\">MLSolver syntax</a>, in <a href=\"http://www.csc.liv.ac.uk/ ullrich/samples/paar2010/pdlProver-Cpdl2-5-3.zip\">pdlProver syntax</a> </li> </ul>","bibtex":"@INPROCEEDINGS{Hustadt+Schmidt@PAAR2010,\n AUTHOR = {Hustadt, Ullrich and Schmidt, Renate, A.},\n TITLE = {A Comparison of Solvers for Propositional Dynamic Logic},\n BOOKTITLE = {Proceedings of the Workshop on Practical Aspect of Automated Reasoning (PAAR-2010)\n [Edinburgh, Scotland, 14 July 2010]},\n YEAR = {2010},\n EDITOR = {Konev, B. and Schmidt, Renate A. and Schulz, Stephan},\n PAGES = {},\n CADDRESS = {Edinburgh, Scotland},\n CYEAR = {2010},\n CMONTH = jul # {~14},\n URL = {Hustadt+Schmidt@PAAR2010.pdf},\n ABSTRACT = {Calculi for propositional dynamic logics have been investigated since\nthe introduction of this logic in the late seventies. Only in recent\nyears have practical procedures been suggested and implemented. In\nthis paper, we compare three such systems, namely, the\nTableau Workbench by Abate, Gor&eacute;, and Widmann\n(2009), the pdlProver system by Gor&eacute; and Widmann (2009), and\nthe MLSolver system by Friedmann and Lange (2009).\n<p>\nThe benchmarking formulae used in this paper are available in\nMLSolver and pdlProver syntax:\n<ul style=\"margin-top: -10; margin-left: 0; padding-left: 20px;\">\n<li>C_PDL¹ (n=5, k=3, p=0.5): \nin <a href=\"http://www.csc.liv.ac.uk/~ullrich/samples/paar2010/mlsolver-Cpdl1-5-3.zip\">MLSolver syntax</a>, \nin <a href=\"http://www.csc.liv.ac.uk/~ullrich/samples/paar2010/pdlProver-Cpdl1-5-3.zip\">pdlProver syntax</a>\n</li>\n<li>C_PDL² (n=5, k=3, p=0.5): \nin <a href=\"http://www.csc.liv.ac.uk/~ullrich/samples/paar2010/mlsolver-Cpdl2-5-3.zip\">MLSolver syntax</a>, \nin <a href=\"http://www.csc.liv.ac.uk/~ullrich/samples/paar2010/pdlProver-Cpdl2-5-3.zip\">pdlProver syntax</a>\n</li>\n</ul>}\n}\n","author_short":["Hustadt, U.","Schmidt, R."],"editor_short":["Konev, B.","Schmidt, R. A.","Schulz, S."],"key":"Hustadt+Schmidt@PAAR2010","id":"Hustadt+Schmidt@PAAR2010","bibbaseid":"hustadt-schmidt-acomparisonofsolversforpropositionaldynamiclogic-2010","role":"author","urls":{"Paper":"http://cgi.csc.liv.ac.uk/~ullrich/publications/Hustadt+Schmidt@PAAR2010.pdf"},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"http://cgi.csc.liv.ac.uk/~ullrich/publications/all.bib?authorFirst=1","dataSources":["WhiGijHmCtTSdLaAj"],"keywords":[],"search_terms":["comparison","solvers","propositional","dynamic","logic","hustadt","schmidt"],"title":"A Comparison of Solvers for Propositional Dynamic Logic","year":2010}