Publication details

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

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               

@INPROCEEDINGS{KaminskiSmolka:2011:HPDL,
  title = {Clausal Tableaux for Hybrid PDL},
  author = {Mark Kaminski and Gert Smolka},
  year = {2011},
  month = {Nov},
  editor = {Hans van Ditmarsch and David Fernández Duque and Valentin Goranko and Wojtek Jamroga and Manuel Ojeda-Aciego},
  publisher = {Elsevier},
  booktitle = {M4M-7},
  series = {ENTCS},
  volume = {278},
  pages = {99-113},
}

Login to edit