下载文档原格式
论自然推理系统P的三种证明方法刘亚婷 兴义民族师范学院数学科学学院摘要：自然推理系统P是逻辑学中很好的一个推理规则，它可以用来解决日常生活、科学领域、社会活动等逻辑推理，它主要有三种证明方法：直接证明法、附加前提证明法和归谬证明法。
用这三种方法推出的结论，都是有效结论，当他的前提条件成立时，结论一定成立。
关键词：自然推理系统；证明；方法 中图分类号：O141 文献识别码：A 文章编号：1001-828X(2017)030-0389-02在数理逻辑中，最重要的就是用数学的方法研究推理。
所谓推理，就是通过一系列已知的命题公式，应用所给的推理规则推出命题公式的过程。
推理又分为公理推理和自然推理，在我们的日常生活中，经常用自然推理来解决一些实际问题。
自然推理是形式系统中的推理之一，我们常称为自然推理系统P。
现将自然推理系统P 定义如下：1.字母表(1)命题变项的符号: p, q, r, …(2) 联结词的符号: ┐,∧,∨， →, ↔(3)逗号与括号: ，, ( )2.合式公式(1) 单个的命题变项和命题常项是合式公式, 称作原子命题公式(2) 若A是合式公式，则 (A)也是合式公式(3) 若A, B是合式公式，则(AB), (AB),(AB), (AB)也是合式公式(4) 有限次地应用(1) --(3)组成的符号串也是合式公式3. 推理规则(1)前提引入: 在证明的任何步骤上都可引入已知前提;(2) 结论引入: 在证明的任何步骤上所得到的结论都可作为后续证明的前提。
(3) 置换规则:在证明的任何步骤上,命题公式都可以用与之等值的公式来置换。
(4)假言推理 (5)附加规则 (6)化简规则A→B A A∧B_ _A__ ∴A∨B ∴A∴ B(7)拒绝式 (8)假言三段论A→B A→B┐B B→C∴┐A ∴A→C(9)析取三段论 (10)构造性二难A∨B A→B┐B C→D∴ A A∨C∴B∨D(11)破坏性二难 (12)合取引入规则A→B AC→D B┐B∨┐D ∴A∧B∴┐A∨┐C那么如何在自然推理系统P中进行证明呢？步骤如下：(1)将原子命题符号化(2)将实际问题的前提A1, A2, …, A k写出来(3)将实际问题的结论B写出来(4)根据自然推理系统P中的推理规则进行判断在自然推理系统P中构造证明时，将形式构造成：前提：A1, A2, …, A k结论：B然后利用直接证明法、附加前提证明法和归谬证明法进行证明。
离散数学结构第3章命题逻辑的推理理论复习第3章命题逻辑的推理理论主要内容1. 推理的形式结构：①推理的前提②推理的结论③推理正确④有效结论2. 判断推理是否正确的⽅法：①真值表法②等值演算法③主析取范式法3. 对于正确的推理，在⾃然推理系统P中构造证明4. ①⾃然推理系统P的定义②⾃然推理系统P的推理规则：前提引⼊规则、结论引⼊规则、置换规则、假⾔推理规则、附加规则、化简规则、拒取式规则、假⾔三段式规则、构造性⼆难规则、合取引⼊规则。
③附加前提证明法④归谬法学习要求1. 理解并记住推理的形式结构的三种等价形式，即①{A1,A2,…,A k}├B②A1∧A2∧…∧A k→B③前提与结论分开写：前提：A1,A2,…,A k结论：B在判断推理是否正确时，⽤②；在P系统中构造证明时⽤③。
2. 熟练掌握判断推理是否正确的三种⽅法（真值表法，等值演算法，主析取范式法）。
3. 牢记P系统中的各条推理规则。
4. 对于给定的正确推理，要求在P系统中给出严谨的证明序列。
5. 会⽤附加前提证明法和归谬法。
3.1 推理的形式结构定义3.1设A1,A2,…,A k和B都是命题公式，若对于A1,A2,…,A k和B中出现的命题变项的任意⼀组赋值，或者A1∧A2∧…∧A k为假，或者当A1∧A2∧…∧A k为真时，B也为真，则称由前提A1,A2,…,A k推出B的推理是有效的或正确的，并称B是有效结论。
⼆、有效推理的等价定理定理3.1命题公式A1,A2,…,A k推B的推理正确当且仅当(A1∧A2∧…∧A k )→B为重⾔式。
A k为假，或者A1∧A2∧…∧A k和B同时为真，这正符合定义3.1中推理正确的定义。
由此定理知，推理形式：前提：A1,A2,…,A k结论：B是有效的当且仅当(A1∧A2∧…∧A k)→B为重⾔式。
(A1∧A2∧…∧A k)→B称为上述推理的形式结构。
从⽽推理的有效性等价于它的形式结构为永真式。
于是，推理正确{A1,A2,…,A k} B可记为A1∧A2∧…∧A k B其中同⼀样是⼀种元语⾔符号，⽤来表⽰蕴涵式为重⾔式。
离散数学自然推理系统在计算机问题中的应用(一)离散数学自然推理系统在计算机问题中的应用应用一：证明算法的正确性离散数学自然推理系统在计算机科学中可以用来证明算法的正确性。
通过使用形式化的数学逻辑和推理规则，可以推导出算法在各种情况下的正确结果。
这有助于开发人员在实现算法之前，预先验证算法的逻辑和正确性，从而提高代码质量和减少错误。
应用二：谓词逻辑在数据库查询中的应用离散数学中的谓词逻辑可以用于数据库查询语言中，以支持高级的查询功能。
谓词逻辑可以描述对象之间的关系和约束条件，通过使用谓词逻辑，可以编写复杂的查询语句，从数据库中检索所需的数据。
这样，离散数学自然推理系统在数据库查询中的应用可以提高查询的灵活性和功能。
应用三：命题逻辑在形式化规约中的应用离散数学中的命题逻辑可以用于形式化规约的描述和验证。
通过使用命题逻辑，可以将复杂的规约问题转化为简单的逻辑表达式，进而验证规约的正确性和一致性。
这种使用离散数学自然推理系统的应用能够帮助开发人员更好地理解和分析规约问题，确保系统设计的正确性。
应用四：图论在网络流优化中的应用离散数学中的图论在计算机网络中有着广泛的应用。
特别是在网络流优化中，图论提供了强大的数学工具和算法。
通过应用图论中的最大流最小割定理以及相关算法，可以实现网络中的资源分配和传输优化，提高网络的吞吐量和效率。
应用五：布尔代数在数字电路设计中的应用离散数学中的布尔代数在数字电路设计中扮演着重要的角色。
通过使用布尔代数的逻辑运算和定理，可以分析、设计和优化数字电路的功能和性能，如门电路、计算机中央处理器等。
这种离散数学自然推理系统在数字电路设计中的应用，对于提高电子设备的性能和可靠性至关重要。
应用六：集合论在数据库和网络安全中的应用离散数学中的集合论在数据库和网络安全中有重要的应用。
通过使用集合论，可以描述和操作各种数据集合，并进行集合运算和关系判断。
这在数据库查询和数据分析中非常有用。
此外，在网络安全领域，集合论也被广泛应用于访问控制和安全策略的建模和验证。
自然推理系统中的假设前提引入与消去规则王太忠【摘要】Hypotheses introduction is the most important characteristic of the system of formalized natural inference. In the natural deduction,the hypothetical premise can be introduced at any time when needed,but it must be eliminated finally because the conclusion can not depend on it. It is a process of syntactic transformation to use the rule for hypotheses elimination to do an inference according to the rule “If A1,A2,…,An├B,then A1,A2,…,An-1├ An→B”,but to understand the principle of work of the rule for hypotheses elimination relates to the discussion on the truth-value relation between premise and conclusion,which belongs to the range of semantic interpretation.% 形式化的自然推理系统最显著的特点就是引入假设前提。
在自然推理中,可以根据需要随时引入假设前提,但是推理的结论不能依赖于假设前提,因此假设前提在其完成了使命后,必须被消去。
运用假设前提消去规则进行推理就是按照“如果A1,A2,…,An├B,那么A1,A2,…,An-1├An→B”的规则进行语形变换的过程,但是理解假设前提消去规则何以能够消去假设前提这个问题,涉及到对前提与结论之间真假制约情况的讨论,属于语义解释的范围【期刊名称】《西昌学院学报（自然科学版）》【年(卷),期】2012(000)002【总页数】5页(P37-41)【关键词】自然推理;假设前提;引入;消去【作者】王太忠【作者单位】昭通师范高等专科学校中文系,云南昭通657000【正文语种】中文【中图分类】O141.11 引言“形式化是现代逻辑最重要的方法，并且是其特色所在。
