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，前提中的和是子句。結論可以用兩個子句和代替。