Publication details

Saarland University Computer Science

Clausal Tableaux for Hybrid PDL

Mark Kaminski, Gert Smolka

Technical Report, Saarland University, March 2010

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.

A revised version of the paper is available.

Download PDF        Show BibTeX               


Login to edit


Webmaster, Wed Sep 16 10:47:00 2009