AIL C5 知识图谱与描述逻辑

语义网络和知识图谱 可以用于表示特定领域中的结构化知识。

• 本体 是一种支持知识共享的、统一的术语体系。
• 描述逻辑 建模 本体。是语义网络和知识图谱推理的逻辑学基础。

语义网络和知识图谱

知识：

• 在基于知识的系统中可以被表示为一组公式集合；
• 通常具有一定结构。e.g 框架，网络。

在网络结构的知识体系中，知识在一个带标签的 有向图 中得到表达：

• 图的结点：实体，可以是对象或概念。
• 图的边：实体间关系
• 两个节点和一条边的三元组：$prop(Ind,Prop,Val)$。
  • 结点$Ind$，主语。
  • 边$Prop$，动词，是一种特性。
  • 结点$Val$，宾语。

建模中的处理：保持二元关系？

语义网络

语义网络是一个图，结点表示对象或概念，弧表示这些对象或概念之间的关系。

知识图谱

知识图谱是一种语义网络，用于描述现实世界的各种实体及其关系。由 结点、边和标签组成。

• 实体：对象，事件，情境，概念等
• 核心：从大数据中提取结构化知识，以语义网络形式展示。

本体与描述逻辑

若要运用知识图谱中的各个元素进行推理，首先必须阐明这些元素及其关系的含义。在计算机领域，通常把符号的含义建构到文档中，即：在计算机中的符号与人脑中的概念之间*建立映射关系*。

• 可以使用统一资源标识符 URI 来表示个体或特性。人们在使用URI时隐含了相关的含义。

• 不同的建模者有不同的术语体系及其含义定义。通常需要建立一个统一的术语体系并阐明其中各个元素的含义来实现知识共享。

本体

统一的术语体系称为本体，可以被理解为一种用于描述特定领域 概念及其关系的形式化规范。

• 关于事物分类的词汇表。
• 分类的组织，e.g subClassOf或 subPropertyOf定义继承关系。
• 一组公理集合，用于限制一些符号的定义以更好反映期望的含义。e.g 一些特性是传递的 / 论域和值域是受限的 / 特性值的数量是受限制的。

描述逻辑

描述逻辑是语义网络的继承和发展。它是一阶逻辑的子集，可以用于本体建模。目前有多种描述逻辑；每种描述逻辑都有自己的表示语言、表达能力和计算复杂性。

• 属性语言 $\cal{AL}$：一种基本的语言，可以表示原子的否定、概念交、全称约束、受限的存 在量化。
• 属性语言$\cal{ALC}$： 是一种代表性的语言，允许有任意的概念。

基本组成元素

描述逻辑中的三种实体:

• 个体 - 一阶逻辑的个体常元。个体名称表示一个领域中的单个个体。
• 概念 - 一阶逻辑的一元谓词。概念表示个体的集合。
• 角色- 一阶逻辑的二元谓词。

公理

本体由一系列句子组成，这些句子被称为公理。

• 公理必须在所描述的情况下为真。

• 公理通常只描述本体所描述的情况的部分知识，可能存在与本体相一致的多种世界状态。即不同于数据库，本体不能完全描述特定的 “情况” 或 “世界的状态”.
• 从逻辑的角度看，不同类型的公理之间没有主要区别。

断言型（ABox）公理：断言事实

ABox 公理可以刻画关于命名个体的知识：它们所属的概念以及它们相互之间的关系。

• 概念断言

$$\begin{align*} \rm Mother(julia)\\ \rm julia:Mother \end{align*}$$

• 角色断言

$$\rm ParentOf(julia,john)$$

术语型 （TBox）公理：表达术语知识

TBox 公理描述概念之间的关系。

• 概念包含

$$\begin{align*} \rm Mother\sqsubseteq Parent \end{align*}$$

• 概念等价 : 两个概念有相同的实例。

$$\rm Person \equiv Human$$

关系型（RBox）公理：建模角色间关系

RBox 公理是关于角色的特性的。

• 角色包含公理

  $$\rm ParentOf \sqsubseteq ancestorOf$$

• 角色等价公理

概念和角色的构造算子

布尔概念构造算子

布尔概念构造算子提供基本的布尔运算。可类比地理解为集合的交集、并集和补集运算，或者逻辑表达式的合取、析取和否定运算。

e.g

$$\begin{align*} \rm Mother &\equiv \rm Female \sqcap Parent\\ \rm Parent &\equiv \rm Father \sqcup Mother\\ \rm Miss &\equiv \rm Female \sqcap \lnot Married \end{align*}$$

角色限制

通过角色限制 形成将概念和角色联系在一起的语句。

e.g 父母是至少一个人的父母：

$$\rm Parent \equiv \exist parentOf.\top$$

除了女性孩子没有其他孩子的人：

$$\rm\forall parentOf.Female \equiv \lnot\exist parentOf.\lnot Female$$

注意，这里包含了根本没有孩子的人。使用

$$\rm Parent \sqcap \forall parentOf.Female \equiv \exist parentOf.\top\sqcap\forall parentOf.Female$$

表示至少有一个孩子而且孩子都是女性的人。

$\cal{ALC}$语法

形式上，每个描述逻辑本体都基于三组有穷的 符号集合：

• $N_C$ - 概念名集合
• $N_R$ - 角色名集合
• $N_O$ - 个体名集合

三元组 $(N_C,N_R,N_O)$ 构成描述逻辑的名字表。

$\cal{ALC}$ 概念集合

$\cal{ALC}$ 概念集合 是满足如下条件的极小集合：

• $\bot$和$\top$是概念，$\bot$表示领域中所有对象的集合。
• $A \in N_C$: 每个原子概念是概念。
• 给定概念$C,D$，角色$R \in N_R$，那么如下是概念:
  • $C \sqcap D$：两个概念的交是一个概念。
  • $C \sqcup D$：两个概念的并是一个概念。
  • $\lnot C$：一个概念的补是一个概念。
  • $\forall R.C$：由一个角色对一个概念的全称约束是一个概念。
  • $\exist R.C$：由一个角色对一个概念的存在约束是一个概念。

$\cal{ALC}$公理

• 术语公理：
  给定概念$C,D$，普通概念包含形如$C \sqsubseteq D$。
  概念等价 当$C \sqsubseteq D$且$D \sqsubseteq C$时，记作$C \equiv D$。
• 断言公理：
  概念断言是一个形如$a : C$ 的句子，其中 $a \in N_O,C$ 是一个概念。
  角色断言是一个形如 $(a, b) : R$的句子，其中 $a, b ∈ N_O,R$是一个角色。

TBox是一组术语公理的有穷集合，ABox 是一组断言公理的有穷集合。

知识库：有序对 $(T,A)$，其中$T$和$A$分别是 TBox 和 ABox。

扩张

给定一个 TBox $\cal{T}$ ，可将$\cal{T}$中的原子概念分为两个集合：

• $\cal{N_T}$:出现于公理左侧的名称符号集合；
• $\cal{B_T}$: 出现于公理右侧的基符号集合。

通常把名称符号称为被定义的概念，而把基符号称为原始概念。

• 有环：$\cal{T}$中存在一个使用自身的原子概念。
• 无环：$\cal{T}$中不存在一个使用自身的原子概念。

当一个 TBox 中的概念定义是无环的时，可通过一组原子概念定义所有其他概念，即将定义右侧的每个名称替换为该名称所代表的概念，通过一个最终停止的迭代过程得到一个术语 TBox $\cal{T}'$，称为T的扩张，它只包含形如 $A \equiv C'$ 的定义，其中 $C'$ 只包含基符号，不包含名称符号。

LEMMA 1

TBox$\cal{T}$与其扩张$\cal{T}'$ 等价。

$\cal{ALC}$语义

一个解释 $\mathcal{I}$由一个集合$\Delta^{\mathcal{I}}$ 和一个解释函数 $·^{\mathcal{I}}$ 组成。$\Delta^{\mathcal{I}}$被称为$\mathcal{I}$的域，$·^{\mathcal{I}}$将每个原子概念$A$ 映射到一个集合$A^{\mathcal{I}} \sube \Delta^{\mathcal{I}}$；将每个原子角色$R$ 映射到二元关系$R^{\mathcal{I}} \sube \Delta^{\mathcal{I}} \times \Delta^{\mathcal{I}}$；将每个个体名称映射到一个元素 $a^{\mathcal{I}} \in \Delta^I$。

在此基础上，非原子概念和非原子角色的语义由原子概念和原子角色的语义来定义。

给定名字表$(N_C,N_R,N_O)$，相应的术语解释 ${\mathcal{I}} = (\Delta^I, ·^I)$：

• 论域：非空集合$\Delta^{\mathcal{I}}$ 。

• 解释函数 $·^{\mathcal{I}}$ 包括如下映射：

  1. 将每个个体$a$映射到一个元素 $a^{\mathcal{I}} \in \Delta^I$；
  2. 将每个概念$A$ 映射到一个集合$A^{\mathcal{I}} \sube \Delta^{\mathcal{I}}$；
  3. 将每个角色$R$ 映射到一个集合$R^{\mathcal{I}} \sube \Delta^{\mathcal{I}} \times \Delta^{\mathcal{I}}$。

  使得

  • $\top^{\mathcal{I}} = \Delta^I$
  • $\bot^{\mathcal{I}} = \phi$
  • $(C\sqcup D)^{\mathcal{I}} = {\it C}^I \cup {\it D}^I$
  • $(C\sqcap D)^{\mathcal{I}} = {\it C}^I \cap {\it D}^I$
  • $(\lnot C)^{\mathcal{I}} = {\Delta}^I - {\it C}^I$
  • $(\forall R.C)^{\cal{I}} = \left\{\it x\in\Delta^{\cal{I}} | \forall y (x,y) \in R^{\cal{I}} \rightarrow y \in C^{\cal{I}}\right\}$
  • $(\exist R.C)^{\cal{I}} = \left\{ x\in\Delta^{\cal{I}} | \exist y \in \Delta^{\cal{I}}:(x,y) \in C^{\cal{I}}\right\}$

请注意角色全称约束的解释定义。$(\forall R.C)^{\cal{I}} = \left\{\it x\in\Delta^{\cal{I}} | \forall y (x,y) \in R^{\cal{I}} \rightarrow y \in C^{\cal{I}}\right\}$意味着对于该集合的任一元素$d$，和任一元素$y\in \Delta^{\mathcal{I}}$，若$(d,y) \in R^{\mathcal{I}}$，则有$y\in C^{\mathcal{I}}$。注意$(d,y) \not\in R^{\mathcal{I}}$时，$(x,y) \in R^{\mathcal{I}} \rightarrow y\in C^{\mathcal{I}}$ 的真值为真。

$\cal{ALC}$推理

概念推理

为一个领域建模时，可通过定义新概念来构建一个术语体系如$\cal{T}$。 此时需要厘清该新概念是否有意义或矛盾。

如果存在某个解释满足$\cal{T}$的公理（i.e$\cal{T}$的模型），使得该概念在该解释中表示一个非空集，那么该概念是有意义的。有意义的概念被称为关于$\cal{T}$可满足的。否则，称为关于$\cal{T}$不可满足的。

• 可满足性：

  设$\cal{T}$是一个TBox。概念 $C$ 是关于$\cal{T}$可满足的，如果存在$\cal{T}$的一个解释 ${\mathcal{I}}$，使得$C^{\mathcal{I}}$ 非空。

可满足是概念的性质，概念间关系包括：包含、等价和不相交。

• 概念包含：

  设$\cal{T}$是一个TBox。关于$\cal{T}$，概念$C$被包含于概念$D$，如果对于$\cal{T}$的每个解释${\mathcal{I}}$，成立$C^{\mathcal{I}} \sube {\it D}^I$。记$C$包含于$D$ 为 ${\cal{T}} \models C \sqsubseteq D$。

• 概念等价：

  设$\cal{T}$是一个TBox。概念$C$与$D$关于$\cal{T}$等价，如果对于$\cal{T}$的每个解释$\cal{I}$，$C^{\cal{I}} = D^{\cal{I}}$， 记作${\cal{T}} \models C \equiv D$。

• 概念不相交：
  设$\cal{T}$是一个TBox。概念$C$与$D$关于$\cal{T}$不相交，如果对于$\cal{T}$的每个解释 $\cal{I}$，$C^{\mathcal{I}} \cap {\it D}^I = \phi$。

  上下文清楚时可省去关于T。

LEMMA 2

包含、等价和不相交三种概念可以被规约到可满足问题。给定概念$CD$ ：

• $C \sqsubseteq D$，当且仅当 $C \sqcap\lnot D$ 不可满足。
• $C \equiv D$，当且仅当 $C \sqcap\lnot D$和$D \sqcap \lnot C$ 均 不可满足。
• $C \sqcap D = \phi$，当且仅当 $C \sqcap D$ 不可满足。

简化推理：去除 TBox

依据$\cal{T}$和$\cal{T}'$的等价性，如果$\cal{T}$可扩张(无环)，则总是可以把关于$\cal{T}$的推理问题规约到关于空 TBox 的推理问题：假设在扩张中$C,D$扩张为$C',D'$，则

• $C$ 关于$\cal{T}$可满足，当且仅当 $C'$ 关于$\cal{T}'$可满足。
• ${\cal{T}} \models C \sqsubseteq D$ ，当且仅当 ${\cal{T}'} \models C' \sqsubseteq D'$。
• ${\cal{T}} \models C \equiv D$当且仅当${\cal{T}} \models C \equiv D$。
• $C$与$D$关于$\cal{T}$不相交 当且仅当 $C'$与$D'$关于$\cal{T}'$不相交。

填充ABox

在设计一个术语体系并使用描述逻辑系统的推理服务进行所有概念可满足性（以及概念间关系转化的可满足性）的检查后，可向 ABox 填充关于个体的断言：概念断言和角色断言。这些知识的表示必须一致。

如果$\cal{T}$可扩张(无环)，则总是可以把ABox的一致性检查规约为扩张的ABox检查。

$\cal{ALC}$表算法

表算法实现：

1. 概念的可满足性检查
2. ABox 的一致性检查：与基于概念的可满足性检查算法类似。
3. 涉及普通包含公理的一致性检查：需要引入可以处理普通包含公理的机制。

概念可满足性检查

首先，算法把待判定的公式转化为否定范式，NNF.

否定范式,NNF

设${\cal K} = ({\cal T, A})$ 为知识库。

• 把$C \equiv D$ 替换为$C \sqsubseteq D$ 和$D \sqsubseteq C$。
• 把$C \sqsubseteq D$ 替换为 $\lnot C \sqcup D$。
• 使用如下$NNF$转换：
  • 原子概念$C$: ${\rm NNF}(C) = C, {\rm NNF}(\lnot C) = \lnot C$
  • ${\rm NNF}(\lnot\lnot C) = {\rm NNF}(C)$
  • ${\rm NNF}(C \sqcup D) = {\rm NNF}(C) \sqcup {\rm NNF}(D)$
  • ${\rm NNF}(C \sqcap D) = {\rm NNF}(C)\sqcap{\rm NNF}(D)$
  • ${\rm NNF}(\lnot(C \sqcup D)) = {\rm NNF}(\lnot C) \sqcap {\rm NNF}(\lnot D)$
  • ${\rm NNF}(\lnot(C\sqcap D)) = {\rm NNF}(\lnot C) \sqcup {\rm NNF}(\lnot D)$
  • ${\rm NNF}(\forall R.C) = \forall R.{\rm NNF}(C)$
  • ${\rm NNF}(\exist R.C) = \exist R.{\rm NNF}(C)$
  • ${\rm NNF}(\lnot \forall R.C) = \exist R.{\rm NNF}(\lnot C)$
  • ${\rm NNF}(\lnot \exist R.C) = \forall R.{\rm NNF}(\lnot C)$

同样的，$\cal K$ 与$\rm NNF({\cal K})$ 在逻辑上是等价的。

表转换规则

$\cal A$是一个 ABox。表转换规则包括：

• 与规则 / $\sqcap$ 规则：如果$x : (C\sqcap D) \in\cal A$，且$\{x : C, x : D\} \not\sube\cal A$，那么${\cal A}' = {\cal A}∪\left\{x : C, x : D\right\}$。
• 或规则 / $\sqcup$ 规则：如果$x : (C\sqcup D) \in\cal A$，且$\{x : C, x : D\} \cap {\cal A} = \phi$，那么${\cal A}' = {\cal A}∪\left\{x : C\right\},{\cal A}'' = {\cal A}∪\left\{x : D\right\}$。
• 存在 / $\exist$ 规则：如果$x:\exist R.C \in \cal A$，而且不存在 $z$ ，$z : C \in A$且$(x, z) : R \in\cal A$，则对于一个新的个体 $y\in{\cal A, A'} = {\cal A} \cup \left\{y : C,(x, y) : R\right\}$。
• 全称 / $\forall$ 规则：如果$x:\forall R.C \in \cal A$且$(x,y):R \in \cal A$，但，$y : C \not\in A$且$(x, z) : R \in\cal A$，则 ${\cal A'} = {\cal A} \cup \left\{y : C\right\}$。

ABox的性质

• ABox的冲突性：
  ABox$\cal A$包含冲突 / 冲突的，若存在个体名 $a$ ，概念$C$使得$\{a: C, a : \lnot C\} \sube \cal A$， 或者$\bot \sube \cal A$。否则称为 无冲突的。

算法从ABox ${\cal A_0} = \{x_0 : C_0\}$ 开始，不断应用表转换规则直到没有更多的规则可应用。

• ABox的完全性：

  $\cal A$是完全的，如果$\cal A$ 包含冲突，或没有一个扩张规则可应用的。

• ABox的一致性：

  $\cal A_0$是一致的，如果不断应用扩张规则得到的完全的$\cal A$ 是无冲突的。$C_0$也是可满足的。
  否则称为不一致的，$C_0$是不可满足的。

Exp：应用表转换规则判断可满足性

e.g 判断

$$(\rm Professor \sqsubseteq (Person\sqcap UniversityEmployee)\sqcup(Person\sqcap\lnot Student))\sqcap(\lnot(Professor\sqsubseteq Person))$$

的可满足性。
PROOF
作$\rm NNF$，令

$$A_0 = \{x :(\rm \lnot Professor \sqcup (Person\sqcap UniversityEmployee)\sqcup(Person\sqcap\lnot Student))\sqcap Professor\sqcap\lnot Person\}$$

证明过程如下：

1. 由$A_0$和与规则，$x : \rm Professor$
2. 由$A_0$和与规则，$x: \rm \lnot Person$
3. 由$A_0$和与规则，$x:\rm \lnot Professor \sqcup (Person\sqcap UniversityEmployee)\sqcup(Person\sqcap\lnot Student)$
   1. 由 3 和或规则，$x : \rm ¬Professor$ (包含冲突)
   2. 由 3 和或规则，$x : \rm (Person\sqcap UniversityEmployee)$
      1. 由 3.2 和与规则，$x:\rm Person$ (包含冲突)
      2. 由 3.2 和与规则，$x : \rm UniversityEmployee$
   3. 由 3 和或规则，$x : \rm Person\sqcap\lnot Student)$
      1. 由 3.3 和与规则，$x : \rm Person$ (包含冲突)
      2. 由 3.3 和与规则，$x: \rm\lnot Student$

所有分支都包含冲突，因此$A_0$ 不可满足。

本算法适用于 TBox 为空的情况。当 TBox 非空且无环时，可通过扩张去掉TBox。

含普通包含的ABox 一致性检查

• 存在多条普通包含公理:

  对于存在多条普通包含公理$(C_1 \sqsubseteq D_1, \cdots , C_n \sqsubseteq D_n)$，只考虑一条公理$\top\sqsubseteq \hat C$（任何个体,包括原有个体和由规则产生的新个体，都必须属于$\hat C$）.

  其中

  $$\hat{C} = (\lnot C_1 \sqcup D_1)\sqcap \cdots \sqcap( \lnot C_n \sqcup D_n)$$

  仅应用上述算法或导致算法的不可终止。如，$A_0 = \{x_0 : A, x_0 : (\exist R.A)\}$ 的一致性检查。

• 存在规则的阻止：

  存在规则应用于个体 $x$ 被一个 ABox$\cal A$中个体 $y$ 阻止，当且仅当 $\{D | D(x) \in {\cal A}\} \sube \{D' | D'(y) \in{\cal A}\}$

Exp：在普通包含公理约束下判断可满足性

e.g设${\cal A_0} = \rm\{Bill : Person\}$，普通包含公理$\rm Person \sqsubseteq\exist hasParent.Person$。证明在普通包 含公理的约束下，$\cal A_0$ 的不可满足性。

1. 由$\cal A_0\rm ,Bill : Person$
2. 由包含公理，$\rm Bill : (\lnot Person\sqcup \exist hasParent.Person)$
3. 由 2 和或规则，$\rm Bill : \lnot Person$ (包含冲突)
4. 由 2 和或规则，$\rm Bill : (\exist hasParent.Person)$
   1. 由 2.2 和存在规则，$\rm (Bill, {\it x_1}) : hasParent$
   2. 由 2.2 和存在规则，$x_1 :\rm Person$
   3. 由包含公理，$x_1 :\rm (\lnot Person\sqcup \exist hasParent.Person)$
   1. 由 2.2.3 和或规则，$x_1 :\rm ¬Person$ (包含冲突)
   2. 由 2.2.3 和或规则，$x_1 :\rm (\exist hasParent.Person)$ (阻止)

所有分支都包含冲突，因此$\cal A_0$ 不可满足。