自然推理系统P.ppt

自然推理系统
数理逻辑的主要任务是用数学的方法来研究推理。所谓推理是指从前提出发推出结论的思维过程，而前提是已知命题公式集合，结论是从前提出发应用推理规则推出的命题公式。
§ 命题逻辑的推理理论
自然推理系统
数理逻辑的主要任务是用数学的方法来研究推理。所谓推理是指从前提出发推出结论的思维过程，而前提是已知命题公式集合，结论是从前提出发应用推理规则推出的命题公式。
§ 命题逻辑的推理理论
一、有效推理
定义 设α1，α2，…，αn，β都是命题公式，
称推理“α1，α2，…，αn推出β”是有效的（或正确的），
如果对α1，α2，…，αn，β中出现的命题变项的任一指派，
若α1，α2，…，αn都真，则β亦真，并称β是有效结论。
否则，称“由α1，α2，…，αn推出β”是无效的或不合理的。
注意：在推理形式中，推理形式的有效与否与前提中命题公式的排列次序无关。
我们将前述推理用更严谨的形式推理系统描述出来 。
怎样在计算机上实现如下的有效推理：
{pq, qr} ├ pr
识别符号p,q,r
识别公式pq, qr, ……
推理方法
定义
一个形式系统I由下面四个部分组成：
（1）非空的字符表集，记作A(I)。
（2）A(I)中符号构造的合式公式集，记作E(I)。
（3）E(I)中一些特殊的公式组成的公理集，记作AX(I)。
（4）推理规则集，记作R(I)。
可以将I记为<A(I),E(I),AX(I),R(I)>.
其中<A(I),E(I)>是I的形式语言系统，<AX(I),R(I)>为I的形式演算系统。
形式系统
符号库（字母表）
（形式）公式
（形式）公理
（形式）推理规则
符号库和形式公式统称为形式语言系统。
形式公理和形式推理规则统称为形式演算系统。
形式系统分为：
（1）自然推理系统：从任意给定的前提出发，应用系统中的推理规则进行推理演算，最后得到结论。
（2）公理推理系统：从若干条给定的公理出发，应用系统中的推理规则进行推理演算，最后得到系统中的重言式，称为定理。
本书只介绍自然推理系统P，它的定义中无公理部分。
自然推理系统P定义如下：
1．字母表
（1）命题变项符号：p，q，r，…,pi，qi，ri，…（2）联结词符号：┐,∧,∨,→,（3）括号和逗号：(,)，，
2．。
3．推理规则（1）前提引入规则：在证明的任何步骤上都可以引入前提。（2）结论引入规则：在证明的任何步骤上所得到的结论都可以作为后继证明的前提。

（3）置换规则：在证明的任何步骤上，命题公式中的子公式都可以用与之等值的公式置换，得到公式序列中的又一个公式。由九条推理定律和结论引入规则还可以导出以下各条推理定律。
（4）假言推理规则（或称分离规则）：由A→B和A，可得B.
若证明的公式序列中已出现过A→B和A，则由假言推理定律(A→B)∧AB可知，B是A→B和A的有效结论。由结论引入规则可知，可将B引入到命题序列中来。
（4）假言推理 用图示表示如下：
（5）附加规则
（6）化简规则