1.5.2 推理证明方法

根据定义1.5.1，判断由前提A推出结论B的方法就是判断A→B是重言式的方法，可以采用不同的证明方法，下面是常用的证明方法，其中，真值表法、等价运算法是基本的方法。

通过写出真值表判断A→B的类型，若A→B是重言式，则由前提A可以推出结论B。

1.真值表法

例1.5.3 证明前提p∨q和可以推出结论q∨r。

证明 根据定义1.5.1，只需证明是重言式。

其真值表如表1.5.2所示。

由真值表可知，是重言式，所以前提p∨q和可以推出结论q∨r。

◀

2.等价演算法

利用命题的等值演算判断A→B的类型，若A→B是重言式，则由前提A可以推出结论B。

例1.5.4 证明q是和p∨q的结论。

证明

当命题公式所含命题变元较多时，上述证明方法较为不便，因而常用演绎法证明推理的有效性。

◀

3.演绎法

演绎法从前提（假设）出发，依据公认的推理规则和推理定律推导出一个结论。在证明过程中，将前提和推理定律匹配，推出结论。判断推出的结论是否为需要证明的结论，如果是，则结束；如果不是，则把推出的结论加入前提集合中，构成一组新的前提，重复上述过程，直到推出需要证明的结论为止。演绎法证明推理问题就是用命题公式序列描述推理过程，其中的每个公式或者是前提，或者是由某些前提得出的结论。在这样的证明中需要引入下面的推理规则。

1）前提引入规则。在推导的过程中，可随时引入前提集合中的任意一个前提。

2）结论引入规则。在推导的过程中，所得到的结论都可作为后续推导的前提。

3）置换规则。在推导的过程中，命题公式的子公式都可以用等值的公式置换。

4）CP规则（附加前提规则）。如果推出的结论形为P→Q，则可以把P放到前提中去，设法推出Q即可。

这些规则与1.5.1节的推理定律和1.3.1节的基本等价公式作为推理和演绎的基础，可以构造一个完整的命题演算推理系统，证明命题逻辑的推理。

例1.5.5 证明（p∨q）∧（p↔r）∧（q→s）⇒s∨r。

证明

例1.5.6 证明，由前提“今天下午有课且今天比昨天冷；只有今天下午没有课，我们才去游泳；如果我们不去游泳，我们就去打篮球；如果我们打篮球，我们就会感到精力充沛”推出结论“我们感到精力充沛”是正确的。

证明 设p表示“今天下午有课”，q表示“今天比昨天冷”，r表示“我们去游泳”，s表示“我们去打篮球”，h表示“我们感到精力充沛”。

则前提为p∧q，，结论是h。

例1.5.7 证明是p→（q→r）和p∧q的结论。

证明

4.附加前提证明法

根据CP规则，如果推出的结论形为P→Q，则可以把P放到前提中去，设法推出Q即可。

例1.5.8 证明r→s是p→（q→s）、、q的结论。

证明 根据CP规则，只需证明s是r、p→（q→s）、、q的结论。

以上证明方法又称直接证明法。在推理问题的构造证明中，有时采用间接证明的方法（又称归谬法）。

5.间接推演法（归谬法）

间接推演法就是把要推出的结论否定后与原来的前提一起使用推出矛盾结论的证明方法。

定义1.5.2 设H₁，H₂，…，H_r是r个命题公式。若H₁∧H₂∧…∧H_r是矛盾式，则称H₁，H₂，…，H_r是不相容的，否则称H₁，H₂，…，H_r是相容的。

如果公式B是由前提H₁，H₂，…，H_r推出的，则是重言式，因此是矛盾式，即H₁，H₂，…，H_r，不相容。因而，若H₁，H₂，…，H_r，不相容，则说明B是公式H₁，H₂，…，H_r的逻辑结论。这种将B作为附加前提推出矛盾的证明方法称为间接推演法（归谬法）。

例1.5.9 用间接法证明p是的结论。

6.归结证明法

例1.5.10 证明蕴涵结论r。

证明

在例1.5.10中利用了归结规则，称为归结证明。归结规则在基于逻辑规则的编程语言中扮演着重要角色。可以用归结规则构建自动定理证明系统。要使用归结规则构造命题逻辑中的证明，前提和结论必须被表示为子句，子句是变元或其否定的析取，如p∨q、等是子句。对于非子句的公式，可以用一个或多个和它等价的子句替换它，如可以用代替公式p→q；对于公式p∨（q∧r），因为p∨（q∧r）⇔（p∨q）∧（p∨r），可以用两个子句p∨q和p∨r代替p∨（q∧r）；可以用两个子句和代替，因为。

例1.5.11 用归结规则证明下面的推理。

如果小张守门或小李上场，则A队获胜；或者A队未获胜，或者A队成为联赛第一名；A队没有成为联赛第一名。因此小张没有守门并且小李没有上场。

证明 设p表示“小张守门”，q表示“小李上场”，r表示“A队获胜”，s表示“A队成为联赛第一名”。

前提：。

结论：。

前提中的，用两个子句和代替（p∨q）→r，前提中的和是子句。结论可以用两个子句和代替。