Clausal Tableaux for Hybrid PDL

摘要

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.