{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T14:29:04Z","timestamp":1777645744327,"version":"3.51.4"},"reference-count":0,"publisher":"SAGE Publications","issue":"1","license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Fundamenta Informaticae"],"published-print":{"date-parts":[[2010,7]]},"abstract":"<jats:p>We reformulate Pratt\u2019s tableau decision procedure of checking satisfiability of a set of formulas in PDL. Our formulation is simpler and its implementation is more direct. Extending the method we give the first ExpTime (optimal) tableau decision procedure not based on transformation for checking consistency of an ABox w.r.t. a TBox in PDL (here, PDL is treated as a description logic). We also prove a new result that the data complexity of the instance checking problem in PDL is coNP-complete.<\/jats:p>","DOI":"10.3233\/fi-2010-299","type":"journal-article","created":{"date-parts":[[2019,12,2]],"date-time":"2019-12-02T23:12:40Z","timestamp":1575328360000},"page":"97-113","source":"Crossref","is-referenced-by-count":7,"title":["Checking Consistency of an ABox w.r.t. Global Assumptions in PDL"],"prefix":"10.1177","volume":"102","author":[{"given":"Linh","family":"Anh Nguyen","sequence":"first","affiliation":[{"name":"Institute of Informatics, Warsaw University, Warsaw, Poland. nguyen@mimuw.edu.pl"}]},{"given":"Andrzej","family":"Sza\u0142as","sequence":"additional","affiliation":[{"name":"Institute of Informatics, Warsaw University, Warsaw, Poland"},{"name":"Department of Computer and Information Science, Link\u00f6ping University, Sweden. andsz@mimuw.edu.pl"}]}],"member":"179","published-online":{"date-parts":[[2010,1]]},"container-title":["Fundamenta Informaticae"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/FI-2010-299","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/FI-2010-299","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T06:33:11Z","timestamp":1777444391000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.3233\/FI-2010-299"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,1]]},"references-count":0,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2010,7]]}},"alternative-id":["10.3233\/FI-2010-299"],"URL":"https:\/\/doi.org\/10.3233\/fi-2010-299","relation":{},"ISSN":["0169-2968","1875-8681"],"issn-type":[{"value":"0169-2968","type":"print"},{"value":"1875-8681","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,1]]}}}