An On-the-fly Tableau-based Decision Procedure for PDL-Satisfiability

Pietro Abate, Rajeev Goré, Florian Widmann

We present a tableau-based algorithm for deciding satisfiability for propositional dynamic logic (PDL) which builds a finite rooted tree with ancestor loops and passes extra inform…