描述邏輯（DL）基礎知識

Logic
邏輯理論其實是一個規範性（normative）的理論，而不是一個描述性的（descriptive）理論。
即，它並非用來描述人類到底是採用何種的形式來推理的，而是來研究人類應該如何有效的進行推理的。
經典邏輯：
命題邏輯proposition logic
一階謂詞邏輯first-order predicate logics / FOL
高階邏輯higher order logics
機率邏輯probability logics
什麼是知識表示？
1. 研究如何用形式化的符號系統來表達特定的知識的一個學術分支。
2. 人工智能的一個分支
3. 還研究如何在計算機系統上實現推理過程
Description Logic 描述邏輯
什麼是描述邏輯（DL）？
一種基於對象的知識表示的形式化。
創建在概念和關係（Role）之上。
概念：對象的集合
關係：對象之間的二元關係
是一階邏輯FOL的一個可斷定的子集
特色：
1. 具備很強的表達能力
2. 是可斷定的，總能保證推理算法終止
------
備受關注的緣由：
1. 清晰的模型-理論機制
2. 適合於經過概念分類學來表示應用領域
3. 提供了有用的推理服務
DL的體系結構：
1. 表示概念和關係（Role）的構造集
2. TBox(Terminology Box)：描述領域結構的公理集，包含概念定義及公理
##能夠理解爲對類別的定義
3. ABox(Assertional Box)：具體個體的公理集，包含概念斷言和關係斷言
##能夠理解爲對個體的定義，以及具體的個體間的關係
4. TBox和ABox上的推理機制：一個基於DL的知識庫就是K=TBox+ABox，簡寫爲 KB(T,A) ##KB即Knowledge Base
DL的基本元素：概念和關係
概念：一個領域的子集。如學生、孩子、哺乳動物等概念
{x|Student(x)},{x|Children(x)}
關係（Role）:屬性，二元關係。如朋友，夫妻
{<x,y>|Friend(x,y)},{<x,y>|Couple(x,y)}
一個例子：圖1：

圖1
TBox:描述領域結構的公理的集合
1. 引入概念的名稱，表示類（一元謂詞）
{x|Student(x)}
2. 聲明包含關係的公理（屬性，二元謂詞）
{<x,y>|Friend(x,y)}
（如圖1）
一個解釋I知足TBox T iff 它知足T中的每一個公理（I entails T ）
## 這裏蘊含符號打不出來，使用 entails 代替
## 邏輯符號表可參見：http://en.wikipedia.org/wiki/Table_of_logic_symbols
ABox：斷言部分，是描述具體清晰的公理的結合
1. 概念斷言：表示一個對象是否屬於某個概念
a:C or C(a)
例如：Student(Tom) 表示Tom是一個學生，也能夠用Tom:Student表示
2. 關係斷言：表示兩個對象是否知足必定的關係
<a,b>:R or R(a,b)
例如：hasChild(John,Mary) 表示John有個孩子叫Mary
一個解釋I知足ABox A iff 它知足A中的每一個公理，記爲 I entails A
## I 被稱做一個解釋（Interpretation），實質上就是一個模型。
一個解釋I知足知識庫∑=<T,A> iff 它知足T和A，記爲 I entails ∑
語法和語義
(如圖2)

圖2
DL中的構造算子
通常的，DL根據提供的構造算子，在簡單的概念和關係上構造出複雜的概念和關係
DL一般包括如下算子：合取、析取、非、存在量詞、全稱量詞
最基本的DL稱爲ALC
例如，ALC中概念Happy-father定義爲：
（如圖3）

圖3
DL中的其餘算子（如圖4）

圖4
DL的演變：
實際應用中，不只要描述概念，還要加強角色的能力。（這裏角色 和 屬性 是一個概念）
具備傳遞性的角色經常使用於構造複合對象。
S：在ALC的基礎上容許部分屬性具備傳遞性
H：歸入屬性包含公理（如「父子關係」包含於「家長孩子關係」），造成屬性（role）分層
I：若S中的屬性的逆勢封閉的，即存在「逆屬性」算子
在SHI的基礎上再添加數量限制、函數線約束或定性數量限定，就有了SHIN, SHIF, SHIQ
DL中的推理
一致性consistency
C關於TBox T是Consistent ？
--- 即檢測是否有T的模型（解釋）I使得C不等於空集。
知識庫KB<T,A>是consistent?
--- 即檢測是否有<T,A>的模型（解釋）I。
可知足性 satisfiability
檢驗一個概念的可知足性，實際就是看是否有解釋使得這個概念成立。
例如：Male ∩ Female
即檢測是否存在這樣的個體既是男的，又是女的。若存在，則可知足，若不存在，不可知足
## see detail in:http://wenku.baidu.com/view/27ff9086bceb19e8b8f6ba2f.html%20-%20## 
## start from PPT-23
包含檢測 subsumption
實例檢測 instance checking
Tableaux算法
可斷定性
計算複雜性

+++++++++++++++++++++++++++++++++++++++++++++++++

其餘關於一階邏輯的介紹見如下連接。

https://wenku.baidu.com/view/966e2cdb6f1aff00bed51e79.html