{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T13:21:26Z","timestamp":1758979286279,"version":"3.41.0"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2014,2,1]],"date-time":"2014-02-01T00:00:00Z","timestamp":1391212800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2014,2]]},"abstract":"<jats:p>\n            This article presents a tableau approach for deciding expressive description logics with full role negation and role identity. We consider the description logic ALBO\n            <jats:sup>id<\/jats:sup>\n            , which is ALC extended with the Boolean role operators, inverse of roles, the identity role, and includes full support for individuals and singleton concepts. ALBO\n            <jats:sup>id<\/jats:sup>\n            is expressively equivalent to the two-variable fragment of first-order logic with equality and subsumes Boolean modal logic. In this article, we define a sound, complete, and terminating tableau calculus for ALBO\n            <jats:sup>id<\/jats:sup>\n            that provides the basis for decision procedures for this logic and all its sublogics. An important novelty of our approach is the use of a generic unrestricted blocking mechanism. Unrestricted blocking is based on equality reasoning and a conceptually simple rule, which performs case distinctions over the identity of individuals. The blocking mechanism ties the proof of termination of tableau derivations to the finite model property of ALBO\n            <jats:sup>id<\/jats:sup>\n            .\n          <\/jats:p>","DOI":"10.1145\/2559947","type":"journal-article","created":{"date-parts":[[2014,3,4]],"date-time":"2014-03-04T13:24:59Z","timestamp":1393939499000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Using tableau to decide description logics with full role negation and identity"],"prefix":"10.1145","volume":"15","author":[{"given":"Renate A.","family":"Schmidt","sequence":"first","affiliation":[{"name":"University of Manchester, Manchester, U.K"}]},{"given":"Dmitry","family":"Tishkovsky","sequence":"additional","affiliation":[{"name":"University of Manchester, Manchester, U.K"}]}],"member":"320","published-online":{"date-parts":[[2014,3,6]]},"reference":[{"volume-title":"Patel-Schneider","year":"2003","author":"Baader Franz","key":"e_1_2_1_1_1"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1013882326814"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_11"},{"volume-title":"Schmidt","year":"2008","author":"Baumgartner Peter","key":"e_1_2_1_4_1"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/10.1.137"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/647837.738480"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/646331.687458"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/648237.753938"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/8.3.265"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/10.1.51"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093894722"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-0609-2_21"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-0897-3_17"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.2307\/421196"},{"volume-title":"Proceedings of the 16th International Joint Conference on Artificial Intelligence (IJCAI'99)","author":"Hustadt Ullrich","key":"e_1_2_1_15_1"},{"key":"e_1_2_1_16_1","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Schmidt","author":"Hustadt Ullrich","year":"2000"},{"volume-title":"Proceedings of the International Workshop on Description Logics (DL'99)","year":"1999","author":"Hustadt Ullrich","key":"e_1_2_1_17_1"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/11853886_44"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1142\/9789812776471_0018"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-25984-8_18"},{"volume-title":"Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI'01)","year":"2001","author":"Massacci Fabio","key":"e_1_2_1_21_1"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19750210118"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/1734953.1734957"},{"key":"e_1_2_1_24_1","unstructured":"OWL. 2004. Web Ontology Language (OWL). http:\/\/www.w3.org\/2004\/OWL. (2004).  OWL. 2004. Web Ontology Language (OWL). http:\/\/www.w3.org\/2004\/OWL. (2004)."},{"key":"e_1_2_1_25_1","unstructured":"OWL 2. 2009. OWL 2 Web Ontology Language: Structural Specification and Functional-Style Syntax. http:\/\/www.w3.org\/TR\/owl2-syntax\/. (2009).  OWL 2. 2009. OWL 2 Web Ontology Language: Structural Specification and Functional-Style Syntax. http:\/\/www.w3.org\/TR\/owl2-syntax\/. (2009)."},{"key":"e_1_2_1_27_1","volume-title":"Vampire. In Proceedings of the 16th Conference on Automated Deduction (CADE-16)","volume":"1632","author":"Riazanov Alexandre","year":"1999"},{"volume-title":"Advances in Modal Logic","author":"Schmidt Renate A.","key":"e_1_2_1_28_1"},{"volume-title":"Deduction and Applications Dagstuhl Seminar Proceedings, Franz Baader, Peter Baumgartner Roberto Nieuwenhuis, and Andrei Voronkov (Eds.), IBFI","year":"2006","author":"Schmidt Renate A.","key":"e_1_2_1_29_1"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-009-9155-4"},{"key":"e_1_2_1_31_1","doi-asserted-by":"crossref","unstructured":"Renate A. Schmidt Ewa Orlowska and Ullrich Hustadt. 2004. Two proof systems for Peirce algebras. In Relational and Kleene-Algebraic Methods in Computer Science: 7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra (RelMiCS'03). Rudolf Berghammer Bernhard Moller and Georg Struth (Eds.) Lecture Notes in Computer Science Vol. 3051 Springer 238--251.  Renate A. Schmidt Ewa Orlowska and Ullrich Hustadt. 2004. Two proof systems for Peirce algebras. In Relational and Kleene-Algebraic Methods in Computer Science: 7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra (RelMiCS'03). Rudolf Berghammer Bernhard Moller and Georg Struth (Eds.) Lecture Notes in Computer Science Vol. 3051 Springer 238--251.","DOI":"10.1007\/978-3-540-24771-5_21"},{"key":"e_1_2_1_32_1","series-title":"Lecture Notes in Computer Science","volume-title":"Schmidt and Dmitry Tishkovsky","author":"Renate","year":"2007"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71070-7_17"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(2:6)2011"},{"key":"e_1_2_1_35_1","first-page":"2","article-title":"E: A brainiac theorem prover","volume":"15","author":"Schulz Stephan","year":"2002","journal-title":"AI Commun."},{"key":"e_1_2_1_36_1","unstructured":"Dmitry Tishkovsky. 2005. The MetTel Prover. http:\/\/www.mettel-prover.org\/. (2005).  Dmitry Tishkovsky. 2005. The M et T el Prover. http:\/\/www.mettel-prover.org\/. (2005)."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/2029664.2029683"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33353-8_41"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_38"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2559947","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2559947","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:10:25Z","timestamp":1750234225000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2559947"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,2]]},"references-count":38,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,2]]}},"alternative-id":["10.1145\/2559947"],"URL":"https:\/\/doi.org\/10.1145\/2559947","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2014,2]]},"assertion":[{"value":"2012-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-03-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}