一阶谓词逻辑

命题逻辑表示法：无法把它所描述的事物的结构及逻辑特征反映出来，也不能把不同事物间的共同特征表述出来。

 个体 x1, x2,…, xn：某个独立存在的事物或者某个抽象的概念；个体可以是常量、变量、函数和谓词
 谓词名 P：刻画个体的性质、状态或个体间的关系

析取（或）朝上；合取（与）朝下

连接词的优先级别从高到低排列： ﹁， ∧， ∨，→，等价

谓词公式表示知识的步骤：
（1）定义谓词及个体。
（2）变元赋值。
（3）用连接词连接各个谓词，形成谓词公式。

---

推理的基本概念

经典推理和非经典推理
单调推理和非单调推理
演绎推理、归纳推理和默认推理
确定性推理和不确定性推理

---

自然演绎推理

从一组已知为真的事实出发，直接运用经典逻辑的推理规则推出结论的过程。

---

归结演绎推理

归结原理由J.A.Robinson由1965年提出。

• 对任一要证明为真公式取非后，证明它不可满足，为此先转化成一种标准型，然后对这个标准型不断使用单一的推理规则，即实行归结，直到导出矛盾。
• 我们说一个问题是可判定的，是指存在一个算法，对问题中的任给的一事例，算法都能给出“是”或“非”的明确答案。命题公式永真性问题是可判定的。
• 我们说一个问题是半可判定的，是指存在一个算法，对问题中的任给的一事例，若它具有某一性质，则算法将不能给出答案。一阶谓词永真性问题是半可判定的。

子句：任何文字的析取式（析取是或，朝上）
合取范式：命题和命题的与PΛ（ P∨Q）Λ（ ～P∨Q）
子句集S：合取范式形式下的子命题（元素）的集合（只能出现析取或，朝上）

◦将命题写成合取范式
◦求出子句集
◦对子句集使用归结推理规则
◦归结式作为新子句参加归结
◦归结式为空子句□ ，S是不可满足的（矛盾），原命题成立。
证明完毕
谓词的归结：除了有量词和函数以外，其余和命题归结过程一样。

SKOLEM标准形
◦前束范式：把所有的量词都提到前面去，然后消掉所有量词。
定义：说公式A是一个前束范式，如果A中的一切量词都位于该公式的最左边（不含否定词），且这些量词的辖域都延伸到公式的末端。
◦量词消去原则：
消去存在量词“”，略去全称量词“”
注意：左边有全称量词的存在量词，消去时该变量改写成为全称量词的函数；如没有，改写成为常量。
◦定理：
谓词逻辑的任意公式都可以化为与之等价的前束范式，但其前束范式不唯一。
◦ SKOLEM标准形定义：
消去量词后的谓词公式。
注意：谓词公式G的SKOLEM标准形同G并不等值。

P∨Q 等价于 ~P=>Q

子句集的求取

1. 消去蕴涵符号：只应用∨和_符号，以A∨B替换A=>B。
2. 减少否定符号的辖域
3. 对变量标准化：合适公式中变量的标准化意味着对哑元改名以保证每个 量词有其自己唯一的哑元。
4. 消去存在量词：若在全称量词辖域内，化为该变量的函数；否则化为常量（大写）
5. 化为前束形
6. 把母式化为合取范式
7. 消去全称量词
8. 消去连词符号∧
9. 更换变量名称

归结推理规则

基子句消解式
◦ 互补文字：若P是原子谓词公式，则称P与~P为互补文字。
◦ 消解式：消去两个子句的互补对，所得的新子句叫做消解式。没有互补对的两子句没有消解式。

含有变量的消解式

置换：为了对含有变量的子句使用归结规则，我们必须找到一个置换，作用于父辈子句使其含有互补文字。
σ={z/x}：把x置换成z

归结反演求解过程

给出一个公式集S和目标公式L，通过反证或反演来求证目标公式L，其证明步骤如下：
（1） 否定L，得~L；
（2） 把~L添加到S中去；
（3） 把新产生的集合{~L，S}化成子句集；
（4） 应用归结原理，力图推导出一个表示矛盾的空子句。
消解树
反演求解过程：
反演树求取对某个问题的答案，其过程如下：
（1）把目标公式的否定产生的每个子句添加到目标公式否定之否定的子句中去。
（2）按照反演树，执行和以前相同的归结，直到在根部得到某个子句止。
（3）用根部的子句作为一个回答语句。

先进行归结，证明结论的正确性；
用重言式代替结论求反得到的子句；
按照证明过程，进行归结；
最后，在原来为空的地方，得到的就是提取的回答。
修改后的证明树称为修改证明树

归结过程的控制策略

给出控制策略，以使仅对选择合适的子句间方可做归结。避免多余的、不必要的归结式出现。或者说，少做些归结仍能导出空子句。

1. 删除策略完备
2. 语义归结：完备一种语义归结策略是将S分成两部分，约定每部分内的子句间不允许做归结。还引入了文字次序，约定归结时其中的一个子句的被归结文字只能是该子句中“最大”的文字
3. 支持集策略：完备想要证明A1∧A2∧A3 => B 成立或 A1∧A2∧A3∧~B 不可满足。分析一下出现矛盾的原因，不会在A1，A2，A3 间发生，自然是出于~B 的引入，于是不必在找不到矛盾的A1，A2，A3 间做归结了。设S的子集T，说T是支持集，如果S-T是可满足的。每次做归结，至少有一个子句来自T或由T导出的归结式。
4. 线性归结：完备首先从子句集S中选取一个称作顶子句的子句C0开始做归结，其次是归结过程中所得到的归结式Ci立即同另一子句Bi进行归结得归结式C i+1。Bi属于S或是已出现的归结式Cj(j，i)。顶子句的选择直接影响着归结的效率
5. 单元归结：不完备每次归结都有一个子句是单元（只含一个文字的）子句或单元因子时的归结称作单元归结。
6. 输入归结：不完备在归结过程中，对两个子句所做的每一次归结，其中必须有一个S的子句时，便称作输入归结。

---

非归结演绎推理

本节内容不考

规则正向演绎系统

事实表达式的与或形变换

事实：把事实表示为非蕴含形式的与或形，不必化简为子句集。
1)利用（W1 =〉 W2）和（~W1∨W2）的等价关系，消去符号=〉。
2) 用狄·摩根（De Morgan）定律把否定符号移进括号内，直到每个否定符号的辖域最多只含有一个谓词为止。
3) 对所得到的表达式进行Skolem化和前束化。
4)对全称量词辖域内的变量进行改名和变量标准化，而存在量词量化变量用Skolem函数代替。
5) 删去全称量词，而任何余下的变量都被认为具有全称量化作用。
主合取元变量换名，使同一变量不出现在事实表达式的不同主要合取式中。

事实的与或图表示

与或图的F规则变换

规则：正向规则演绎系统应用规则作用于表示事实的与或图，改变与或图的结构，从而产生新的事实。为应用方便起见，规定规则的形式为：L=>W
1)L是单文字，W是与或形的唯一公式
2) L和W中的所有变量都是全称量词量化的，默认的全称量词作用于整个蕴含式
3) 各条规则中的变量各不相同，而且规则中的变量与事实表达式中的变量也不相同

作为终止条件的目标公式

在正向演绎系统中，目标公式规定为文字的析取形式，当一个目标文字和与或图中的一个文字匹配时，可以将表示该目标文字的节点通过匹配弧连接到与或图中相应文字的节点上。表示目标文字的结点称为目标结点。当演绎系统产生的与或图包括一个在目标结点上结束的解图时，系统便成功的结束。

规则逆向演绎系统

(1)目标：化简为不含蕴含符号的文字与或形
对目标进行Skolem化，即消去全称量词，变量受存在量词约束，对主析取元中的变量换名
目标用与或树表示，其中，“开口朝下”对应树中“与”，“开口朝上”对应树中“或”
(2)事实表达式：文字的合取
(3)规则形式 ： W  L, 其中L为单文字，如形为： W  L 1  L 2，则变换为：
W  L 1 和 W L 2
从目标出发，逆向应用规则，到得到事实节点为结束条件的一致解图为止

目标表达式的与或形式

目标表达式的与或图表示

与或图的B规则变换

作为终止条件的事实节点的一致解图

逆向系统中的事实表达式均限制为文字合取形，它可以表示为一个文字集。当一个事实文字和标在该图文字节点上的文字相匹配时，就可把相应的后裔节点添加到该与或图中去。这个事实节点通过标有mgu的匹配弧与匹配的子目标文字节点连接起来。同一个事实文字可以多次重复使用（每次使用不同变量），以便建立多重事实节点。逆向系统成功的终止条件是与或图包含有某个终止在事实节点上的一致解图。

规则双向演绎系统

小结

要看开始状态和目标状态谁多？人们希望从小的状态集出发朝大的状态集推理，找解更容易。
受到方向分枝因素大小的约束，一般朝分枝因素低的方向推理。
还决定于是否需向用户证实程序的推理过程。若是则选择方向更加符合用户的思考方法

---

知识图谱

---

不确定推理

本节内容不做要求（毕竟都没学哇）

---

好好忍耐，不要沮丧，如果春天要来，大地会使它一点一点地完成

---

• 声明：以上内容来源于老师上课讲述和ppt，未经允许不得转载