Publication details

Saarland University Computer Science

Clausal Tableaux for Hybrid PDL

Mark Kaminski, Gert Smolka

M4M-7, Vol. 278 of ENTCS, pp. 99-113, Elsevier, November 2011

We present the first tableau-based decision procedure for PDL with nominals. The procedure is based on a prefix-free clausal tableau system designed as a basis for gracefully degrading reasoners. The clausal system factorizes reasoning into regular, propositional, and modal reasoning. This yields a modular decision procedure and pays off in transparent correctness proofs.

DOI: 10.1016/j.entcs.2011.10.009

This paper is a revised version of the following report.

Download PDF        Show BibTeX               


Login to edit


Legal notice, Privacy policy