U. Hustad and R. A. Schmidt (2010): ``A Comparison of Solvers for Propositional Dynamic Logic.'' In B. Konev, R. A. Schmidt and S. Schulz, editors, Proceedings of the Workshop on Practical Aspects of Automated Reasoning (PAAR 2010) [Edinburgh, Scotland, July 14, 2010].
Abstract, BibTeX, Full text.

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).

The benchmarking formula used in this paper are available in MLSolver and pdlProver syntax:


Logic and Computation Group at the Department of Computer Science, University of Liverpool
Maintained by Ullrich Hustadt, U.Hustadt@csc.liv.ac.uk, last updated Thursday, 08-Aug-2013 18:17:54 BST © 1998-2004 by Ullrich Hustadt.