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
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;
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
DOI :
10.1109/KSE.2009.12
