Publication details

Saarland University Computer Science

A Goal-Directed Decision Procedure for Hybrid PDL

Mark Kaminski, Gert Smolka

Journal of Automated Reasoning 52(4):407-450, April 2014

We present the first goal-directed decision procedure for hybrid PDL. The procedure is based on a modular approach that scales from basic modal logic with eventualities to hybrid PDL. The approach is designed so that nominals and eventualities are treated orthogonally. To deal with the complex programs of PDL, the approach employs a novel disjunctive program decomposition. In arguing the correctness of our approach, we employ the novel notion of support generalizing the standard notion of Hintikka sets.

DOI: 10.1007/s10817-013-9294-5

Download PDF        Show BibTeX               


Login to edit


Webmaster, Wed Sep 16 10:47:00 2009