自动推理

自动定理证明
假言推理(Modus Ponens, MP): \[\frac{a,\quad a\Rightarrow b}{b}\]
And-Introduction, AI: \[\frac{a,\quad b}{a\land b}\]
全称量词实例化(Universal instantiation, UI)\[\frac{\forall v\quad a}{Subst(\{v/g\},a)}\]其中v为变元(variable)，g为基项（没有变量的项, ground term）。此实例化可说明所有的变元v替换成基项g后，a仍成立。

存在量词实例化(Existential instantiation, EI)\[\frac{\exists v\quad a}{Subset(\{v/k\},a)}\]其中k应当是一个从未在知识库中出现过的常量符号k，称为Skolen常数。

前向链接(Forward Chaining)与反向链接(Backward Chaining)
合取范式(Conjunctive Normal Form, CNF): 由文字(literals)的析取子句进行合取得到的语句，如\((A\lor\lnot B)\land(B\lor C\lor \lnot D)\).
限定子句(Definite clause): 恰好只含一个正文字的析取式。如\(A\lor B\lor \lnot C\)不是，但\(\lnot A \lor\lnot B\lor C\)是限定子句。限定子句可以改写成蕴含式的形式，如上例为\(A\land B\Rightarrow C\).
Horn子句：至多含一个正文字的析取式。
目标子句(Goal clause): 不含正文字的析取式。

前向链接：判定单个命题词是否被限定子句的知识库所蕴含。
枚举所有现有知识库中命题符号可以推出的命题，如果不在KB中，就将新结论加入，直到要查询的命题词(query)被证明。通过维护每个命题符号的蕴含前提的命题符号个数进行推断。

反向链接与前向链接类似，从查询的命题符号开始推理。为了证明q，检查q是否已知或者证明q的所有前提。
前向链接和反向链接对Horn KB是可靠且完备的，但对一阶逻辑FOL不是完备的。

归结(Resolution)
归结是一个反证过程：为证明\(KB\vDash a\), 归结为\(KB\land\lnot a\)是不可满足的。归结需要用合取范式CNF的形式，将两个子句\(C_1,C_2\)归结为\(C\), 称为归结式子句(resolvent). 当归结式子句为空时得证（相当于推出矛盾）。
对于两个CNF \(C_1,C_2\)中分别包括的互补文字\(A,\lnot A\)，归结后可消去；相同文字可合并成一个。

命题逻辑中，语句到CNF的转化：
1. 用两个\(\rightarrow\)的合取消去\(\Leftrightarrow\);
2. 用\(A\lor\lnot B\)消去\(B\Rightarrow A\);
3. 使用摩根律将\(\lnot\)移到文字前；
4. 使用分配律调整\(\land,\lor\)为CNF。
归结证明算法：首先将clauses初始化为\(KB\land\lnot a\)的CNF表示。
用new\(=\{\}\)维护新产生的子句。
1. 对每一对clauses中的\(C_i,C_j\)，归结为新的子句resolvents.
| a. 如果resolvents为空语句，则命题得证。
| b. 否则，将resolvents 加入new中。
2. 判断是否有news\(\subseteq\) clauses.
| a. 如果成立，则无新子句产生，证明失败。
| b. 否则，将clauses \(\cup\) new赋给 clauses; 并回到1.

合一(Unification)
合一置换是指使不同的逻辑表示变得相同的置换。
合一算法Unify以两条语句为输入，如果存在合一置换，则返回之：\(Unify(p,q)=\theta\), 其中\(Subst(\theta,p)=Subst(\theta,q)\).
如果两个语句使用了相同的变量x，则不能进行合一置换，但可以通过新的命名解决这一问题。

对每一对可以合一的表达式，存在唯一的最一般合一置换(Most General Unifiers, MGU).

    所属分类：人工智能     发表于2022-05-22