@inproceedings{070f54b59d9649cfb9703c1f7898a826,
title = "Tableaux and algorithms for propositional dynamic logic with converse",
abstract = "{\textcopyright} Springer-Verlag Berlin Heidelberg 1996.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.",
author = "{De Giacomo}, G. and F. Massacci",
year = "1996",
doi = "10.1007/3-540-61511-3_117",
language = "English",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "613--627",
editor = "J.K. Slaney and M.A. McRobbie",
booktitle = "Automated Deduction – Cade-13 - 13th International Conference on Automated Deduction, Proceedings",
note = "13th International Conference on Automated Deduction, CADE 1996 ; Conference date: 30-07-1996 Through 03-08-1996",
}