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: 

## start from PPT-23

包含检测 subsumption

实例检测 instance checking

Tableaux算法

可判定性

计算复杂性

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

其他关于一阶逻辑的介绍见以下链接。

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