自然推理系统中推理证明的两种新思路

尹慧琴，唐耀平

（湖南科技学院理学院，永州 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 结语

本文推导出两个新的自然推理系统下的推理证明方法。第一种为结论后件否定引入法，是针对结论为蕴涵式的情形，引入后件的否定作为附加前提，推出结论前件的否定即可。第二种方法为结论析取项否定引入法，通常针对结论为析取式的情形，引入析取式其中一个子式的否定作为前提，推出结论析取式中的另一个子式即可。两种新方法对于结论的一些特殊形式能简化证明步骤，证明思路清晰，有助于提高解决推理问题的证明的效率。