推理的形式结构

推理有前提和结论。记前提为$A_1,A_2,\cdots,A_n$，结论为$B$，则由前提推出结论可以抽象地表示为一个逻辑表达式

该推理正确等价于上式无条件为真，也就是说

推理有以下几种方法

• 真值表枚举法：对所有的变量枚举所有可能的取值，证明该表达式恒为真
• 等值演算法：根据逻辑学定理将该表达式变形，直到可以确定其为真
• 构造证明法: 从前提出发，严格按照推理规则构造命题序列，序列的最后一条是结论

包含蕴涵的重言式可以列举如下，供推理使用。蕴含符号的左侧为真就意味着右侧为真，欲证明右侧为真可以证明左侧为真

定律名称	表达式
附加律	$A \vDash (A \lor B)$
化简律	$(A \land B) \vDash A$
假言推理	$(A \Rightarrow B) \land A \vDash B$
拒取式	$(A \Rightarrow B) \land \neg B \vDash \neg A$
析取三段论	$(A \lor B) \land \neg B \vDash A$
假言三段论	$(A \Rightarrow B) \land (B \Rightarrow C) \vDash (A \Rightarrow C)$
等价三段论	$(A \Leftrightarrow B) \land (B \Leftrightarrow C) \vDash (A \Leftrightarrow C)$
构造性二难	$(A \Rightarrow B) \land (C \Rightarrow D) \land (A \lor C) \vDash (B \lor D)$
构造性二难(特殊)	$(A \Rightarrow B) \land (\neg A \Rightarrow B) \vDash B$
破坏性二难	$(A \Rightarrow B) \land (C \Rightarrow D) \land (\neg B \lor \neg D) \vDash (\neg A \lor \neg C)$

推理规则

规则名称	表达式	描述
前提引入规则	$\begin{aligned} A \\ \therefore A \end{aligned}$	一个命题可以直接推出自身
结论引入规则	$\begin{aligned} \vdash B \\ \therefore A \vdash B \end{aligned}$	如果结论成立，则添加前提无影响
置换规则	$\begin{aligned} A \iff B \\ \therefore B \iff A \end{aligned}$	等价命题可以交换位置
假言推理规则	$\begin{aligned} A \Rightarrow B \\ A \\ \therefore B \end{aligned}$	前提成立则结论必然成立
附加规则	$\begin{aligned} A \\ \therefore A \lor B \end{aligned}$	单个命题可以推出或关系
合取消去规则	$\begin{aligned} A \land B \\ \therefore A \end{aligned}$	合取中的某一项可以被单独推出
拒取式规则	$\begin{aligned} A \Rightarrow B \\ \neg B \\ \therefore \neg A \end{aligned}$	如果结论不成立，则前提必然不成立
假言三段规则	$\begin{aligned} A \Rightarrow B \\ B \Rightarrow C \\ \therefore A \Rightarrow C \end{aligned}$	前提的传递性推导出最终结论

归结证明

形式上看是消去了变量 $p$ ，利用它可以从条件中消去结论中不出现的变量进而完成证明

证明$A_1\land\cdots\land A_n\Rightarrow B$恒为真等价于证明下式为假

利用反证法，假定它是真的，推出矛盾（0）即可。由此归结证明的过程可以描述如下

1. 将每个前提都转化为合取范式，即一些简单析取式以“或”的形式连接，进而得到一系列简单析取式形式的前提，记为$A_1,A_2,\cdots,A_t$
2. 将结论的反 $\neg B$ 转化为合取范式，即$\neg B=B_1\land B_2\land\cdots\land B_s$
3. 认为这些$B$都是真的，以$A_1,A_2\cdots A_t,B_1,\cdots B_s$为条件，使用归结推出矛盾（0）

一个证明的例子是

首先将前提转化为合取

将结论转化为合取

希望利用前提和结论推出0

先消去$p$

那么就有$~\neg q\lor r,~\neg r\lor s,~\neg s,~q\lor r$，消去$q$

那么$~\neg r\lor s,~\neg s,~r$，再消去$r$

那么$s,~\neg s$。实际上到这里已经出现矛盾了，不过从程序上来说还是推导到$0$为止

即完成了证明。关于归结法有定理

不过它的时间复杂度是指数级的

前向链接与反向链接

逻辑学中将命题抽象为符号，称其为正文字，将其否定称为负文字。鉴于蕴含等值式

$$A\Rightarrow B\equiv \neg A\lor B$$

若$A$是一些正文字的与，即简单合取式$A=a_1\land a_2\cdots \land a_n$，那么由于摩根定律有

也就是说，如果一个析取式中只有一个正文字

它会等价于一个蕴含式

称其为确定子句

若允许全是负文字，则得到了霍恩子句

由于归结会消去两个子句中的一个正文字和对应负文字，因而确定子句或霍恩子句的归结是封闭的，即任意两个确定子句或霍恩子句归结，得到的仍是确定子句或霍恩子句

前向链接算法用于处理确定子句（即蕴涵式）构成的知识库推理问题。如果已知了一个知识库KB，其中是一系列的确定子句。为了描述方便，定义蕴涵式中

$a_1, a_2\cdots , a_n$为前件，$B$为结论。希望查询命题Q是否能被推理，可以依照下面的步骤

0. 初始化一个确定事件集合，用于保存已经确认为真的事实。对于知识库中每一个确定子句，维护其不在确定事件集合中的前件数目
1. 取出知识库中全部前件已知的确定子句（即不在确定事件集合中的前件数目为零），将其结论添加入已知事件集中，将其从知识库中删除
2. 重复1直到命题Q被添加入已知事件集或是知识库为空

也可以采取反向链接算法，它是自顶向下的，即查询以Q为结论的所有蕴涵式是否存在一个其前提都为真，尝试递归证明它们。反向链接算法是目标驱动的，适合解决明确的问题，有时复杂度会远远小于前向链接