Tableaux and algorithms for propositional dynamic logic with converse

G. De Giacomo, F. Massacci

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

Abstract

© 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.
Original languageEnglish
Title of host publicationAutomated Deduction – Cade-13 - 13th International Conference on Automated Deduction, Proceedings
EditorsJ.K. Slaney, M.A. McRobbie
PublisherSpringer Verlag
Pages613-627
DOIs
Publication statusPublished - 1996
Externally publishedYes
Event13th International Conference on Automated Deduction, CADE 1996 - New Brunswick, United States
Duration: 30 Jul 19963 Aug 1996

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference13th International Conference on Automated Deduction, CADE 1996
Country/TerritoryUnited States
CityNew Brunswick
Period30/07/963/08/96

Fingerprint

Dive into the research topics of 'Tableaux and algorithms for propositional dynamic logic with converse'. Together they form a unique fingerprint.

Cite this