SRIQ and SROIQ are Harder than SHOIQ
SRIQ and SROIQ are Harder than SHOIQ
复制标题
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
Yevgeny Kazakov
中科院分区：
文献类型：
--
作者：
Yevgeny Kazakov
我们确定了DL SROIQ中（有限模型）推理的复杂性为N2ExpTime-complete。我们还证明了DL sr中的（有限模型）推理是2ExpTime-hard的。DL sr是SROIQ的一个片段，没有名义、数量限制和逆角色。从SHIQ到SROIQ在本文中，我们研究了DL SROIQ中推理的复杂性，该逻辑被选为owl2的候选逻辑。SROIQ作为SRIQ的扩展在[1]中引入，SRIQ本身在[2]中作为RIQ[3]的扩展引入。这些论文提出了基于表格的程序，并证明了它们的健全性、完备性和终止性。与SHOIQ的子语言相比，其计算复杂性目前已经被很好地理解了[0]，到目前为止，除了从它们的子语言继承的硬度结果外，几乎对SROIQ、SRIQ和RIQ的复杂性一无所知：SROIQ是SHOIQ的扩展，SRIQ和RIQ是SHIQ的扩展，ExpTime-hard。困难是由于复杂的角色包含公理R1◦···◦Rn v R，导致表过程中的指数膨胀。在本文中，我们通过证明SRIQ和SROIQ中的推理比SHIQ和SHOIQ中的推理要困难得多来证明这种爆炸基本上是不可避免的。我们假设读者熟悉DL SHOIQ[5]。SHOIQ签名是一个元组Σ = （CΣ， RΣ， IΣ），由原子概念集CΣ、原子角色RΣ和个体IΣ组成。SHOIQ解释是一对I =(∆I，·I)，其中∆I为称为I域的非空集，·I为解释函数，对每个A∈CΣ赋一个子集AI，对每个r∈RΣ赋一个关系rI，对每个r∈RΣ赋一个元素AI，对每个A∈IΣ赋一个元素AI∈∆I。解释I是有限的iff∆I是有限的。角色可以是某个r∈RΣ，也可以是一个逆角色r−。对于每个r∈RΣ，我们设Inv(r) = r−和Inv(r−)= r。SHOIQ RBox是角色包含公理（RIA） R1 v r、传递公理Tra(r)和功能公理Fun(r)的有限集合r，其中R1和r是角色。设vR为关系vR在R1 vR R iff R1 vR∈R上的自反传递闭包或？除非2ExpTime = NExpTime，在这种情况下，SROIQ比SHOIQ 1（即OWL 1.1）更难：http://www.webont.org/owl/1.1发票(R1) v发票(R)∈R .角色年代被称为简单(关于R)如果没有角色R, R vR和交易(R)∈R或交易(发票(R))∈R .给定一个RBox R, SHOIQ的集合概念是最小的设置包含>,⊥,,{},¬C, C uD C tD,∃阻容,∀阻容,> nS.C,和6 nS.C,那里是一个原子的概念,一个个体,C和D概念,R, S一个简单的角色关于R n一个非负整数。SHOIQ TBox是广义概念包含公理（gci） C v D的有限集合T，其中C和D是概念。我们把C≡D写成C v D和D v C的缩写。SHOIQ ABox是一个有限集合，由概念断言C(A)和角色断言R（A, b）组成，其中A和b是来自IΣ的个体。SHOIQ本体是一个三重O = (R， T，A)，其中R是SHOIQ RBox， T是SHOIQ TBox， A是SHOIQ ABox。解释I以通常的方式[5]扩展到复杂的角色、复杂的概念、公理和断言。I是SHOIQ本体O的一个模型，如果O中的每个公理和断言在I中都满足。对于O的某个（有限）模型I，如果CI 6=∅，概念C在w.r.t O中是（有限）可满足的。众所周知[6,4]，SHOIQ的概念可满足性问题是nexptime完备的。SROIQ[1]在几个方面扩展了SHOIQ。(1)给出了普遍作用U，解释为总关系：UI =∆I ×∆I。(2)它允许否定角色断言R（a, b）。(3)它引入了概念构造函数∃S。自我解释为{x∈∆I | < x, x >∈SI}，其中S是一个简单的角色。(4)它允许新的角色公理Sym(R), Ref(R), Asy(S), Irr(S), Disj(S1, S2)，其中S(i)是简单的角色，它限制RI是对称的或自反的，SI是不对称的或非自反的，或者SI 1和S2是不相交的。(5)最后，它允许形式为R1◦····Rn v R的复杂角色包含公理，该公理要求RI 1···RI n RI，其中◦为二元关系的通常组合。对简单角色的概念进行了调整，以确保角色组合不能隐含任何简单角色。SRIQ[2]是sriiq不带标称的片段。构造函数(1)-(4)不会在SROIQ中引入太多困难——SHOIQ[5]的现有表过程可以相对容易地进行调整以支持新的构造函数。在dl中处理复杂的角色包含公理变得更加困难。首先，除了DL EL[7]之外，复杂ria的无限制使用很容易导致模态和描述逻辑的不可判定[8,3]。因此，在SROIQ中引入了特殊的语法限制以恢复可判决性。角色上的正则序是角色上的非自反传递二元关系<e:1>，使得R1 <e:1> R2 iff Inv(R1) <e:1> R2。一个RIA R1····Rn v R若不包含全称角色U且：(i) n = 2且R1 = R2 = R，或（ii） n = 1且R1 = Inv(R)，或（iii） Ri <s:1> R对于1≤i≤n，或（iv） R1 = R且Ri <s:1> R对于1(5)>≡(B1 U∀R)，则称它是<s:1>正则的。¬B1 u∀r；B1) (6) Bi−1 u∀r。¬Bi−1≡(Bi u∀r。■■■■■■■■Bi), 1 < i≤n (7) Axiom(3)负责使用原子概念z将计数器初始化为零。Axiom(4)可以通过检查E是否成立来检测计数器是否达到最终值2−1。因此，利用公理(5)，我们可以表示当且仅当一个元素的计数器没有达到最终值时，它有一个r后继元素。公理(6)和(7)表示计数器如何在r上递增：公理(6)表示计数器的最低位总是翻转；公理(7)表示，当且仅当下位从1变为0时，计数器的任何其他位被翻转。引理1。设0为包含公理(3)-(7)的本体。则对于O， x∈ZI的每一个模型I =（∆I，·I）存在xi∈∆I，且0≤I < 2，使得x = x0且< xi - 1, xi >∈rI对于每一个1≤I < 2的I， c(xi) = I。现在我们用类似的思想在模型中执行双指数长链。然而，这一次，w
We identify the complexity of (finite model) reasoning in the DL SROIQ to be N2ExpTime-complete. We also prove that (finite model) reasoning in the DL SR—a fragment of SROIQ without nominals, number restrictions, and inverse roles—is 2ExpTime-hard. 1 From SHIQ to SROIQ In this paper we study the complexity of reasoning in the DL SROIQ—the logic chosen as a candidate for OWL 2. SROIQ has been introduced in [1] as an extension of SRIQ, which itself was introduced previously in [2] as an extension of RIQ [3]. These papers present tableau-based procedures for the respective DLs and prove their soundness, completeness and termination. In contrast to sub-languages of SHOIQ whose computational complexities are currently well understood [4], almost nothing was known, up until now, about the complexity of SROIQ, SRIQ and RIQ except for the hardness results inherited from their sub-lanbuages: SROIQ is NExpTime-hard as an extension of SHOIQ, SRIQ and RIQ are ExpTime-hard as extensions of SHIQ. The difficulty was caused by complex role inclusion axioms R1 ◦ · · · ◦Rn v R, which cause exponential blowup in the tableau procedure. In this paper we demonstrate that this blowup was essentially unavoidable by proving that reasoning in SRIQ and SROIQ is exponentially harder than in SHIQ and SHOIQ. We assume that the reader is familiar with the DL SHOIQ [5]. A SHOIQ signature is a tuple Σ = (CΣ , RΣ , IΣ) consisting of the sets of atomic concepts CΣ , atomic roles RΣ and individuals IΣ . A SHOIQ interpretation is a pair I = (∆I , ·I) where ∆I is a non-empty set called the domain of I, and ·I is the interpretation function, which assigns to every A ∈ CΣ a subset AI ⊆ ∆I , to every r ∈ RΣ a relation rI ⊆ ∆I × ∆I , and to every a ∈ IΣ , an element aI ∈ ∆I . The interpretation I is finite iff ∆I is finite. A role is either some r ∈ RΣ or an inverse role r−. For each r ∈ RΣ , we set Inv(r) = r− and Inv(r−) = r. A SHOIQ RBox is a finite set R of role inclusion axioms (RIA) R1 v R, transitivity axioms Tra(R) and functionality axioms Fun(R) where R1 and R are roles. Let vR be the reflexive transitive closure of the relation vR on roles defined by R1 vR R iff R1 v R ∈ R or ? Unless 2ExpTime = NExpTime, in which case just SROIQ is harder than SHOIQ 1 A.k.a. OWL 1.1: http://www.webont.org/owl/1.1 Inv(R1) v Inv(R) ∈ R. A role S is called simple (w.r.t. R) if there is no role R such that R vR S and either Tra(R) ∈ R or Tra(Inv(R)) ∈ R. Given an RBox R, the set of SHOIQ concepts is the smallest set containing >, ⊥, A, {a}, ¬C, C uD, C tD, ∃R.C, ∀R.C, >nS.C, and 6nS.C, where A is an atomic concept, a an individual, C and D concepts, R a role, S a simple role w.r.t. R, and n a non-negative integer. A SHOIQ TBox is a finite set T of generalized concept inclusion axioms (GCIs) C v D where C andD are concepts. We write C ≡ D as an abbreviation for C v D and D v C. A SHOIQ ABox is a finite set consisting of concept assertions C(a) and role assertions R(a, b) where a and b are individuals from IΣ . A SHOIQ ontology is a triple O = (R, T ,A), where R is a SHOIQ RBox, T a SHOIQ TBox, and A a SHOIQ ABox. The interpretation I is extended to complex role, complex concepts, axioms, and assertions in the usual way [5]. I is a model of a SHOIQ ontology O, if every axiom and assertion in O is satisfied in I. A concept C is (finitely) satisfiable w.r.t. O if CI 6= ∅ for some (finite) model I of O. It is well-known [6, 4] that the problem of concept satisfiability for SHOIQ is NExpTime-complete. SROIQ [1] extends SHOIQ in several ways. (1) It provides for the universal role U , which is interpreted as the total relation: UI = ∆I ×∆I . (2) It allows for negative role assertions ¬R(a, b). (3) It introduces a concept constructor ∃S.Self interpreted as {x ∈ ∆I | 〈x, x〉 ∈ SI} where S is a simple role. (4) It allows for new role axioms Sym(R), Ref(R), Asy(S), Irr(S), Disj(S1, S2) where S(i) are simple roles, which restrict RI to be symmetric or reflexive, SI to be asymmetric or irreflexive, or SI 1 and S I 2 to be disjoint. (5) Finally, it allows for complex role inclusion axioms of the form R1 ◦ · · · ◦Rn v R, which require that RI 1 ◦ · · · ◦ RI n ⊆ RI where ◦ is the usual composition of binary relations. The notion of simple roles is adjusted to make sure that no simple role can be implied by a role composition. SRIQ [2] is the fragment of SROIQ without nominals. The constructors (1)–(4) do not introduce too many difficulties in SROIQ— the existing tableau procedure for SHOIQ [5] can be relatively easily adapted to support the new constructors. Dealing with complex role inclusion axioms in DLs turned out to be more difficult. First, with an exception of the DL EL [7], the unrestricted usage of complex RIAs easily leads to undecidability of modal and description logics [8, 3]. Therefore special syntactic restrictions have been introduced in SROIQ to regain decidability. A regular order on roles is an irreflexive transitive binary relation ≺ on roles such that R1 ≺ R2 iff Inv(R1) ≺ R2. A RIA R1 ◦ · · · ◦ Rn v R is said to be ≺-regular, if it does not contain the universal role U and either: (i) n = 2 and R1 = R2 = R, or (ii) n = 1 and R1 = Inv(R), or (iii) Ri ≺ R for 1 ≤ i ≤ n, or (iv) R1 = R and Ri ≺ R for 1 (5) > ≡ (B1 u ∀r.¬B1) t (¬B1 u ∀r.B1) (6) Bi−1 u ∀r.¬Bi−1 ≡ (Bi u ∀r.¬Bi) t (¬Bi u ∀r.Bi), 1 < i ≤ n (7) Axiom (3) is responsible for initializing the counter to zero using the atomic concept Z. Axiom (4) can be used to detect whether the counter has reached the final value 2 − 1, by checking whether E holds. Thus, using axiom (5), we can express that an element has an r-successor if and only if its counter has not reached the final value. Axioms (6) and (7) express how the counter is incremented over r: axiom (6) expresses that the lowest bit of the counter is always flipped; axioms (7) express that any other bit of the counter is flipped if and only if the lower bit is changed from 1 to 0. Lemma 1. Let O be an ontology containing axioms (3)–(7). Then for every model I = (∆I , ·I) of O and x ∈ ZI there exist xi ∈ ∆I with 0 ≤ i < 2 such that x = x0 and 〈xi−1, xi〉 ∈ rI for every i with 1 ≤ i < 2, and c(xi) = i. Now we use similar ideas to enforce double-exponentially long chains in the model. This time, however, w