| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 421796 | Electronic Notes in Theoretical Computer Science | 2011 | 15 Pages |
Abstract
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
