Affiliations: [a] Division of Knowledge and System Engineering for ICT, Faculty of Information Technology, Ton Duc Thang University, Ho Chi Minh City, Vietnam. [email protected] | [b] Institute of Informatics, University of Warsaw, Banacha 2, 02-097 Warsaw, Poland. [email protected]
Correspondence:
[*]
Address for correspondence: Division of Knowledge and System Engineering for ICT, Faculty of Information Technology, Ton Duc Thang University, No. 19, Nguyen Huu Tho Street, Tan Phong Ward, District 7, Ho Chi Minh City, Vietnam
Abstract: We present the first direct tableau decision procedure for graded PDL, which uses global caching and has ExpTime (optimal) complexity when numbers are encoded in unary. It shows how to combine checking fulfillment of existential star modalities with integer linear feasibility checking for tableaux with global caching. As graded PDL can be used as a description logic for representing and reasoning about terminological knowledge, our procedure is useful for practical applications.
