DocumentCode
507490
Title
An Optimal Tableau Decision Procedure for Converse-PDL
Author
Nguyen, Linh Anh ; Szalas, Andrzej
Author_Institution
Inst. of Inf., Univ. of Warsaw, Warsaw, Poland
fYear
2009
fDate
13-17 Oct. 2009
Firstpage
207
Lastpage
214
Abstract
We give a novel tableau calculus and an optimal (EXPTIME) tableau decision procedure based on the calculus for the satisfiability problem of propositional dynamic logic with converse. Our decision procedure is formulated with global caching and can be implemented together with useful optimization techniques.
Keywords
computability; optimisation; process algebra; converse-PDL; global caching; optimal tableau decision procedure; optimization techniques; propositional dynamic logic; satisfiability problem; tableau calculus; Calculus; Informatics; Information science; Knowledge engineering; Knowledge representation; Logic; Page description languages; Systems engineering and theory; Tree graphs; CPDL; global caching; tableaux;
fLanguage
English
Publisher
ieee
Conference_Titel
Knowledge and Systems Engineering, 2009. KSE '09. International Conference on
Conference_Location
Hanoi
Print_ISBN
978-1-4244-5086-2
Electronic_ISBN
978-0-7695-3846-4
Type
conf
DOI
10.1109/KSE.2009.12
Filename
5361706
Link To Document