描述逻辑从表到自动机的转换：决策过程与ALCQI系统

### 描述逻辑从表到自动机的转换：决策过程与ALCQI系统 #### 1. ALC概念可满足性的复杂度 在描述逻辑中，已经证明表系统SALC对于ALC概念相对于（通用）TBox的可满足性问题是ExpTime可允许的，同时也是可靠且p-完备的（对于某个多项式p）。由此可以直接得出推论：ALC概念相对于TBox的可满足性问题属于ExpTime复杂度类。 #### 2. 基于表系统的决策过程 之前描述的表系统不能直接用作基于表的决策过程，因为规则的应用可能不会终止。不过，在某些自然条件下，添加一个简单的循环检测机制可以将其转变为终止的决策过程。这些过程在结构上与描述逻辑中标准的基于表的算法类似，比如FaCT和RACER等系统所基于的算法。与上一节构造的ExpTime算法不同，这里得到的过程通常不是最坏情况最优的，但更易于实现和优化。 ##### 2.1 递归表系统 为了实现这一转变，首先需要定义递归表系统。设输入集为I，表系统S = (NLE, EL, ·S, R, C) 用于I。S被称为递归的，当且仅当满足以下条件： 1. S是可允许的（见相关定义）。 2. 可以有效地计算iniS(Γ)。 3. 对于每个模式P，可以有效地检查对于所有模式P'，P' ∼ P是否意味着R(P') = ∅；如果不是这种情况，则可以有效地确定一个规则P' →R {P1, ..., Pk} 和一个双射π，使得P' ∼π P。 4. 对于每个模式P，可以有效地检查是否存在冲突触发器P' ∈ C，使得P' ∼ P。 与之前的定义相比，主要区别在于条件3，它现在要求除了检查规则的适用性之外，当有规则适用时，还能有效地应用至少一个规则。此外，在应用规则时实际上不需要计算elS(Γ) 和nleS(Γ) 集合。可以验证，表系统SALC是递归的。 ##### 2.2 f - 完备性 定义一个更宽松的f - 完备性概念。设f : N → N是一个递归函数。表系统S对于属性P是f - 完备的，当且仅当对于任何Γ ∈ P，存在一个饱和且无冲突的S - 树，其出度受f(|Γ|) 限制。由于已经证明SALC对于某个多项式p是p - 完备的，所以SALC对于由该多项式诱导的可计算函数f显然是f - 完备的。 ##### 2.3 阻塞机制 为了实现循环检测，引入阻塞的概念。给定一个S - 树T = (V, E, n, ℓ)，用E∗表示E的传递自反闭包。如果存在不同的u, v ∈ V，使得uE∗x，vE∗x，且n(u) = n(v)，则称节点x ∈ V被阻塞。这对应于各种描述逻辑表算法中使用的“相等阻塞”技术。 ##### 2.4 决策过程 基于上述定义，给出属性P的决策过程： ```plaintext Preconditions: Let I be a set of inputs, P ⊆ I a property, f a recursive function, and S a recursive tableau system for I that is sound and f - complete for P. Algorithm: Return true on input Γ ∈ I if the procedure tableau(T) defined below returns true for at least one initial S - tree T for Γ. Otherwise return false. procedure tableau(T) If P ∼ T, x for some P ∈ C and node x in T or the out - degree of T exceeds f(|Γ|), then return false. If no rule is applicable to a non - blocked node x in T, then return true. Take a non - blocked node x in T and a rule P →R {P1, ..., Pk} with P ∼ T, x. Let Ti be the result of applying the above rule such that Pi ∼ Ti, x, for 1 ≤ i ≤ k. If at least one of tableau(T1), tableau(T2), ..., tableau(Tk) returns true, then return true. Return false. ``` 这个过程的规则和节点选择是“不关心”的非确定性的，即对于算法的可靠性和完备性，选择应用哪个规则到哪个节点并不重要。 ##### 2.5 过程有效性验证 可以验证该算法的各个步骤是有效的： - 输入Γ的初始树可以有效地计算，因为根据递归表系统定义的条件2，可以有效地计算iniS(Γ)。 - 第一个“if”语句中的条件可以有效地检查，因为根据定义的条件4和f是递归函数。 - 规则的适用性可以通过定义的条件3的第一部分进行检查。 - 最后，根据条件3的第二部分，可以有效地选择一个规则并将其应用到节点x。 ##### 2.6 算法性质证明 - **终止性**：假设满足上述决策过程的前提条件，对于任何输入Γ ∈ I，算法都会终止。因为输入Γ的初始树数量是有限的且可以有效计算，所以只需证明tableau过程在任何初始树上都会终止。在每次步骤中，如果过程不立即返回真或假，则会向树中添加一个节点或某个节点x的n(x) 适当增加。由于对于任何节点x和在tableau运行期间构造的任何树，n(x) ⊆ ℘(nleS(Γ))，所以只需证明构造的树的出度和深度是有界的。树的出度受f(|Γ|) 限制，并且由于规则不会应用于被阻塞的节点，E - 路径的长度不超过2|nleS(Γ)|。 - **可靠性**：如果算法对于输入Γ返回真，则Γ ∈ P。当算法返回真时，它会终止于一个无冲突的S - 树T，其出度不超过f(|Γ|)，并且没有规则适用于非阻塞节点。由于S对于P是可靠的，所以只需证明存在一个饱和且无冲突的S - 树。通过构造一个与Γ兼容的无冲突且饱和的S - 树T'，可以证明这一点。 - **完备性**：如果Γ ∈ P，则算法对于输入Γ返回真。因为S对于P是f - 完备的，所以存在一个无冲突且饱和的S - 树T，其出度不超过f(|Γ|)。可以使用T来“引导”算法找到一个出度至多为f(|Γ|)、无冲突触发器适用且没有规则适用于非阻塞节点的S - 树。 #### 3. ALCQI表系统 作为一个更具表达力的描述逻辑示例，考虑ALCQI，它在ALC的基础上扩展了限定数量限制和逆角色。 ##### 3.1 ALCQI的语法和语义 设NC和NR是两两不相交且可数无限的概念名和角色名集合。ALCQI角色集定义为ROLALCQI := NR ∪ {r− | r ∈ NR}。