自然推理系統中推理證明的兩種新思路

尹慧琴，唐耀平

（湖南科技學院理學院，永州 425100）

0 引言

數理邏輯是《離散數學》課程中很重要的內容，其中自然推理系統中形式結構下的推理的證明是難點。一般教材[1]在介紹了常規的推理證明方法之后，還特意給出了歸謬法和附加提前法這兩種針對推理結論公式特殊形式的證明方法。這兩種方法確實能有效地進行推理的證明，某些情況下要比常規的推理證明要簡化，學生也容易理解接受。本文基于結論公式的特殊形式，在命題邏輯自然推理系統中對歸謬法和附加前提法進行了進一步的改進。

1 預備知識

（1）自然推理系統

自然推理屬“演繹推理”，由前提命題的合取（∧）蘊涵（→）結論命題。自然推理系統包括字母表、合式公式和推理規則，其特點是從任意給定的前提命題出發，應用系統中的推理規則進行推理演算，最后得到的命題公式是推理的結論。

（2）附加前提法

若推理的結論為蘊涵式，其推理的形式結構為如下形式：此時可將結論中的前件作為推理的前提，使結論為B。即把推理的形式結構改寫為：

文獻[1]證明了（*）式和（**）式是等值的，因而若（**）式是重言式則（*）式也是重言式。此種將結論的前件作為前提推出結論后件的推理方法即為附加前提法。

（3）歸謬法

若推理的形式結構為如下形式：

此時可將結論的否定?B作為推理的前提，若能推出矛盾式來則說明推理正確。文獻[1]證明了A1∧A2∧…∧Ak→B與 ?（A1∧A2∧…∧Ak∧?B）是等值 的 ，即A1∧A2∧…∧Ak∧?B為 矛 盾 式 時 ，A1∧A2∧…∧Ak→B必為重言式。此種將結論的否定作為附加前提引入并推出矛盾式的證明方法為歸謬法。數學上常使用的反證法即為歸謬法。

2 結論后件否定引入法（INLC）

如果推理的結論是蘊涵式，其推理的形式結構如為：此時不像附加前提法那樣將結論的前件作為附加前提引入，而是將結論的后件作為附加前提進行拓展，可以得到如下結論。

對（1）進行等值演算得：

從推理的形式結構來看，在（2）式中，原來結論中得后件的否定?E已經轉化為前提，如果能證明（2）式為重言式，則為（1）式也為重言式。我們稱這種將結論蘊涵式中的前件的否定?E作為推理的邏輯結論，將結論的后件的否定?F作為推理的結論的證明方法稱為結論后件否定引入法（INLC）。例1 為該方法的應用實例。

例1 只要小智是三好學生，小智就會刻苦學習。所以如果小智是三好學生或刻苦學習，小智就刻苦學習。

設p：小智是三好學生，q：小智刻苦學習，則前提和結論符號化為：

前提：p→q

結論：(p∨q)→q

解法一：附加前提法

因為q為結論后件，所以推理正確。

解法二：結論后件否定引入法

推理出的結果?(p∨q)為結論前件的否定，與結論后件否定引入法有效結論一致，所以該命題推理是有效的。

分析：該題用直接證明法需使用一系列置換規則，且思路不清晰，推理過程如同等值演算，失去了自然推理系統中推理證明的意義。而附加前提法與結論后件否定引入法相比較，附加前提法依然需要使用一些置換規則，結論后件否定引入法則思路更清晰，且推理步驟要少。

3 結論析取項否定引入法（INDC）

如果推理的結論是析取式，運用命題邏輯推理定律直接推理難以得出結果來，此時我們綜合借鑒歸謬法和附加前提法的思路對推理方法進行拓展。

設推理形式結構如下：

對（3）式進行等值演算得：

從推理的形式結構來看，在（4）式中，原來結論析取式的某一個子公式的否定?E已經轉化為前提，如果能證明（4）式為重言式，則為（3）式也為重言式。我們稱這種將結論析取式一子公式的否定?E為前提，將結論析取式另一子公式F作為推理的結論的證明方法為結論析取項否定引入法（INDC）。例2 為該方法的應用實例。

例2 每年到了冬天，小雪就會去滑雪。只有每年到了冬天，小雪才不會和家人泡溫泉。所以小雪泡溫泉或去滑雪。

設p：每年到了冬天，q：小雪會去滑雪。r：小雪和家人泡溫泉。

前提：p→q，?r→p

結論：q∨r

解法一：歸謬法

因為?q∧q為矛盾式，所以推理正確。

解法二：結論析取項否定引入法

分析：由題意可知，直接證明會比較復雜，運用結論析取項否定引入法則比較簡潔。如下：

推理出的結果r為結論析取式另一子公式，與結論析取項否定引入法有效結論一致，所以該命題推理是有效的。

分析：該題用直接證明法也需使用一系列置換規則，且思路不清晰，推理過程如同等值演算，失去了自然推理系統中推理證明的意義。而歸繆法與結論析取項否定引入法相比較，歸繆法推理步驟較多，結論后件否定引入法推理步驟少且思路清晰。

4 結語

本文推導出兩個新的自然推理系統下的推理證明方法。第一種為結論后件否定引入法，是針對結論為蘊涵式的情形，引入后件的否定作為附加前提，推出結論前件的否定即可。第二種方法為結論析取項否定引入法，通常針對結論為析取式的情形，引入析取式其中一個子式的否定作為前提，推出結論析取式中的另一個子式即可。兩種新方法對于結論的一些特殊形式能簡化證明步驟，證明思路清晰，有助于提高解決推理問題的證明的效率。