Campus Event Calendar
Event Entry
New for: D2, D3
What and Who
A Comparison of Solvers for Propositional Dynamic Logic
Ullrich Hustadt
University of Liverpool
Talk
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI
Public Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Thursday, 26 August 2010
14:00
60 Minutes
E1 4
024
Saarbrücken
Abstract
Decision procedures 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 talk I will give a general overview of dynamic
logic itself and describe key aspects of decision procedures for the
satisfiability problem in dynamic logic. The focus of the talk will
be on approaches to the construction of benchmarking formulae for the
evaluation of implemented decision procedures. The benchmarking approach
presented in the talk is not specific to dynamic logics, but is intended
to be a general methodology for the evaluation of solvers for
non-classical logics. As a case study I will then present results of such
an evaluation for the current generation of implemented decision procedures
for propositional dynamic logic, namely, the Tableau Workbench by Abate,
Gore, and Widmann (2009), the pdlProver system by Gore and Widmann (2009),
and the MLSolver system by Friedmann and Lange (2009).
investigated since the introduction of this logic in the late seventies.
Only in recent years have practical procedures been suggested and
implemented. In this talk I will give a general overview of dynamic
logic itself and describe key aspects of decision procedures for the
satisfiability problem in dynamic logic. The focus of the talk will
be on approaches to the construction of benchmarking formulae for the
evaluation of implemented decision procedures. The benchmarking approach
presented in the talk is not specific to dynamic logics, but is intended
to be a general methodology for the evaluation of solvers for
non-classical logics. As a case study I will then present results of such
an evaluation for the current generation of implemented decision procedures
for propositional dynamic logic, namely, the Tableau Workbench by Abate,
Gore, and Widmann (2009), the pdlProver system by Gore and Widmann (2009),
and the MLSolver system by Friedmann and Lange (2009).
Contact
Jennifer Müller
900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 08/23/2010 13:00 -- Created document.