Tableaux and algorithms for propositional dynamic logic with converse
| Author(s) : | Fabio Massacci, |
| Publisher : | N/A |
| Publication Date : | 1996 |
| ISSN : | N/A |
| Abstract : | Abstract. This paper presents a prefixed tableaux calculus for Propositional Dynamic Logic with Converse based on a combination of different techniques such as prefixed tableaux for modal logics and model checkers for mu-calculus. We prove the correctness and completeness of the calculus and illustrate its features. We also discuss the transformation of the tableaux method (naively NEXPTIME) into an EXPTIME algorithm. 1, |