命题逻辑的推理理论,证明方法

1、. 武汉大学国际软件学院唐存琛 刘峰12.4 命题逻辑推理理论n2.4.1 推理的形式结构推理的形式结构n推理及其形式结构推理及其形式结构n推理定律推理定律n2.4.2 自然推理系统自然推理系统Pn自然推理系统的定义自然推理系统的定义n证明方法证明方法. 武汉大学国际软件学院唐存琛 刘峰22.4.1 推理的形式结构推理的形式结构一、什么是推理一、什么是推理定义定义2.19 设设A1，A2 ， ，Ak ，B都是命题公式，若对于都是命题公式，若对于每组赋值每组赋值, A1 A2 Ak为假为假, 或者当或者当A1 A2 Ak为真时，为真时，B也为真也为真, 则称由前提则称由前提A1，A2，, Ak推

2、推B的的推推理有效理有效或或推理正确推理正确, 并称并称B是是有效的结论。有效的结论。. 武汉大学国际软件学院唐存琛 刘峰3定理定理2.8 由前提由前提A1, A2, , Ak 推出推出B 的推理正确当且仅当的推理正确当且仅当 A1 A2 Ak B为重言式为重言式.12kAAAB如果把（如果把（A1 A2 Ak ） B为永真式记为：为永真式记为：上式的含义？上式的含义？. 武汉大学国际软件学院唐存琛 刘峰4二、推理的形式结构二、推理的形式结构定义定义2.20 称（称（A1 A2 Ak ） B为由前提为由前提 A1, A2, , Ak推结论推结论 B 的推理的形式结构。的推理的形式结构。推理的形

3、式结构一般有以下三种：推理的形式结构一般有以下三种： 形式形式(1) A1 A2 Ak B 形式形式(2) 前提前提: A1, A2, , Ak 结论结论: B 形式形式(3) A1， A2 ， ， Ak B. 武汉大学国际软件学院唐存琛 刘峰5n真值表法真值表法n等值演算法等值演算法n主析取范式法主析取范式法n构造证明法构造证明法判断推理是否正确的方法判断推理是否正确的方法:真值表的方法参见真值表的方法参见P.67例例2.23。. 武汉大学国际软件学院唐存琛 刘峰6例例1 判断下面推理是否正确判断下面推理是否正确:(1) 若今天是若今天是1号号, 则明天是则明天是5号号. 今天是今天是1号号

4、. 所以所以, 明天明天是是5号号. ()pqpq解解 设设 p: 今天是今天是1号号, q: 明天是明天是5号号 推理的形式结构为推理的形式结构为证明证明 用等值演算法用等值演算法 ()()()()()()pqpqpqpqpqpqpqpqppqpqqpqT 所以，原推理正确。所以，原推理正确。. 武汉大学国际软件学院唐存琛 刘峰7例例1 (2) 若今天是若今天是1号号, 则明天是则明天是5号号. 明天是明天是5号号. 所以所以, 今天是今天是1号。号。()pqqp解解 设设 p: 今天是今天是1号号, q: 明天是明天是5号号 推理的形式结构为推理的形式结构为证明证明 用主析取范式法用主析取

5、范式法 023()()()()()()pqqppqqppqqppqpqpqpqmmm 这不是一个永真式，这不是一个永真式，01是该公式成假的赋值，是该公式成假的赋值，所以推理不正确。所以推理不正确。. 武汉大学国际软件学院唐存琛 刘峰8三、推理规则三、推理规则1、推理规则的定义、推理规则的定义BAAAn,21BAAAn21 是一个是一个推理规则推理规则，当且仅当当且仅当 ，其中其中, A1, A2, , An 称称为推理规则的为推理规则的前提前提，B 称为推理规则的称为推理规则的结论。结论。. 武汉大学国际软件学院唐存琛 刘峰91）附加规则）附加规则2）化简规则）化简规则3）MP规则规则（假言

6、推理）（假言推理）4）拒取式）拒取式BAAABABBAA,ABBA,2、常用的推理规则、常用的推理规则. 武汉大学国际软件学院唐存琛 刘峰105）析取三段论）析取三段论6）假言三段论）假言三段论7）合取引入）合取引入8）构造性二难）构造性二难DBCADCBA,BABA,CACBBA,ABBA,2、常见的推理规则（续）、常见的推理规则（续）. 武汉大学国际软件学院唐存琛 刘峰11n注意：注意：（1）推理规则中出现的）推理规则中出现的A、B、C 等是元语言符号；等是元语言符号；（2）直接引用而不需证明，只要说明所引用规则的名称；）直接引用而不需证明，只要说明所引用规则的名称；（3）24个永真公式每

7、个都可以等效为个永真公式每个都可以等效为2个推理规则。个推理规则。. 武汉大学国际软件学院唐存琛 刘峰122.4.2 自然推理系统自然推理系统P自然推理系统自然推理系统P由下述由下述3部分组成部分组成:1. 字母表字母表 (1) 命题变项符号命题变项符号: p,q,r, pi,qi,ri, (2) 联结词联结词: , , , , (3) 括号与逗号括号与逗号: ( ), ,2. 合式公式合式公式一、自然推理系统一、自然推理系统P的定义的定义. 武汉大学国际软件学院唐存琛 刘峰133. 推理规则推理规则 (1) 前提引入规则前提引入规则 (2) 结论引入规则结论引入规则 (3) 置换规则置换规则

8、 (4) 假言推理规则假言推理规则 (5) 附加规则附加规则 (6) 化简规则化简规则一、自然推理系统一、自然推理系统P的定义（续）的定义（续）(7) 拒取式规则拒取式规则 (8) 假言三段论规则假言三段论规则(9) 析取三段论规则析取三段论规则(10)构造性二难推理构造性二难推理规则规则(11) 破坏性二难推理破坏性二难推理规则规则 (12) 合取引入规则合取引入规则. 武汉大学国际软件学院唐存琛 刘峰14()()pqqrrp 证证例例2 证明证明前提前提前提前提、，假言三段，假言三段前提前提、，拒取式，拒取式pqqrprrp . 武汉大学国际软件学院唐存琛 刘峰15二、证明方法二、证明方法

9、 用推理的概念说明一些证明方法的正确性。用推理的概念说明一些证明方法的正确性。 为了证明为了证明 ，只需证明，只需证明 A 永假永假即可。即可。（2）后件真证明法）后件真证明法 为了证明为了证明 ，只需证明，只需证明 B 永真永真即可。即可。（1）前件假证明法）前件假证明法BABA. 武汉大学国际软件学院唐存琛 刘峰16（3）直接证明法）直接证明法 为了证明为了证明 ，只需证明若，只需证明若 A 为真为真，则，则 B 亦为真亦为真。 为了证明为了证明 ，只需证明若，只需证明若 B 为假为假，则，则 A 亦为假。亦为假。（4）间接证明法）间接证明法BABA. 武汉大学国际软件学院唐存琛 刘峰17

10、（5）分情况证明法）分情况证明法只需证明对任意的只需证明对任意的 ，均有，均有 。为了证明为了证明 , （6）附加前提证明法）附加前提证明法只需证明只需证明为了证明为了证明 , BAi)(nii1BAAAn21BAAAAn21BAAAAn21. 武汉大学国际软件学院唐存琛 刘峰18附加前提证明法的说明：附加前提证明法的说明：理由理由: (A1 A2 Ak)(CB) ( A1 A2 Ak) ( C B) ( A1 A2 Ak C) B (A1 A2 Ak C)B欲证明欲证明 等价地证明等价地证明前提前提: A1, A2, , Ak 前提前提: A1, A2, , Ak, C结论结论: CB 结论

11、结论: B. 武汉大学国际软件学院唐存琛 刘峰19不相容的概念：不相容的概念： 定义定义 若若 是可满足式，则称公是可满足式，则称公式集式集 是是相容的相容的（或（或一致的一致的），否），否则，称之为则，称之为不相容的不相容的。nAAA21nAAA,21. 武汉大学国际软件学院唐存琛 刘峰20（7）反证法（归谬法）反证法（归谬法）为了证明为了证明 BAAAn21即证明即证明是永假式是永假式BAAAn21只需证明只需证明是不相容的是不相容的,BAAAn21. 武汉大学国际软件学院唐存琛 刘峰21归谬法归谬法(反证法反证法)的说明的说明理由理由: A1 A2 AkB (A1 A2 Ak) B (A

12、1 A2 AkB)括号内部为矛盾式当且仅当括号内部为矛盾式当且仅当 (A1 A2 AkB)为重言式为重言式欲证明欲证明前提：前提：A1, A2, , Ak 结论：结论：B将将 B加入前提加入前提, 若推出矛盾若推出矛盾, 则得证推理正确则得证推理正确. . 武汉大学国际软件学院唐存琛 刘峰22证证SPRSPQRQP,例例3 证明证明前提前提附加前提附加前提、，假言推理、，假言推理前提前提、，拒取式、，拒取式、，析取三段论、，析取三段论前提前提、，拒取式，拒取式、，CPPQRPQRQPQRSRSPS . 武汉大学国际软件学院唐存琛 刘峰23证证PSRRQQP)(),(),(例例4 证明证明假设前

13、提假设前提，E1前提前提、，假言推理，假言推理前提前提、，析取三段论，析取三段论前提前提，化简，化简、，合取引入，合取引入 是一个永假式，因此，原推理正确。是一个永假式，因此，原推理正确。()PPPQQQRRRSRRR . 武汉大学国际软件学院唐存琛 刘峰24直接证明法举例直接证明法举例例例5 在自然推理系统在自然推理系统P中构造下面推理的证明中构造下面推理的证明:前提前提: 结论结论:证明：证明： ,()pq qr pssrpq(1)(2)(3)(4)(5)pssppqq前提前提前提前提(1)、(2)拒取式拒取式前提前提(3)、(4)析取三段论析取三段论. 武汉大学国际软件学院唐存琛 刘峰2

14、5(6)(7)(8)()qrrrpq前提前提(5)、(6)假言推理假言推理(7)、(4)合取合取. 武汉大学国际软件学院唐存琛 刘峰26例例6 构造推理的证明构造推理的证明: 若明天是星期一或星期三若明天是星期一或星期三, 我就有课我就有课. 若有课若有课, 今天必需备课今天必需备课. 我今天下午我今天下午没备课没备课. 所以所以, 明天不是星期一和星期三明天不是星期一和星期三. 解解 设设 p:明天是星期一明天是星期一, q:明天是星期三，明天是星期三， r:我有课，我有课， s:我备课我备课前提前提: (p q)r, rs, s结论结论: pq pqr. 武汉大学国际软件学院唐存琛 刘峰2

15、7前提前提: (p q)r, rs, s结论结论: pq 证明：证明： rs 前提引入前提引入 s 前提引入前提引入 r 拒取式拒取式 (p q)r 前提引入前提引入 (p q) 拒取式拒取式 pq 置换置换 结论有效结论有效, 即明天不是星期一和星期三即明天不是星期一和星期三. 武汉大学国际软件学院唐存琛 刘峰28附加前提证明法举例附加前提证明法举例欲证明欲证明 等价地证明等价地证明前提前提: A1, A2, , Ak 前提前提: A1, A2, , Ak, C结论结论: CB 结论结论: B. 武汉大学国际软件学院唐存琛 刘峰29例例7 构造下面推理的证明构造下面推理的证明:前提前提: p

16、 q, q r, rs结论结论: ps证明：证明： p 附加前提引入附加前提引入 p q 前提引入前提引入 q 析取三段论析取三段论 q r 前提引入前提引入 r 析取三段论析取三段论 rs 前提引入前提引入 s 假言推理假言推理 推理正确推理正确, , ps是有效结论是有效结论. 武汉大学国际软件学院唐存琛 刘峰30归谬法归谬法(反证法反证法)举例举例欲证明欲证明前提：前提：A1, A2, , Ak 结论：结论：B将将 B加入前提加入前提, 若推出矛盾若推出矛盾, 则得证推理正确则得证推理正确. . 武汉大学国际软件学院唐存琛 刘峰31例例8 构造下面推理的证明构造下面推理的证明前提前提:

17、(p q) r, rs, s, p ；结论；结论: q证明：用归缪法证明：用归缪法 q 结论否定引入结论否定引入 rs 前提引入前提引入 s 前提引入前提引入 r 拒取式拒取式 (p q) r 前提引入前提引入 (p q) 析取三段论析取三段论 pq 置换置换 p 析取三段论析取三段论. 武汉大学国际软件学院唐存琛 刘峰32 p 前提引入前提引入 p p 合取合取推理正确推理正确, , q是有效结论是有效结论. 武汉大学国际软件学院唐存琛 刘峰33应用实例应用实例1 分析下列事实分析下列事实“如果我有很高的收如果我有很高的收入，那么我就能资助许多贫困学生；如果我能资入，那么我就能资助许多贫困学

18、生；如果我能资助许多贫困学生，那么我很高兴；但我不高兴，助许多贫困学生，那么我很高兴；但我不高兴，所以我没有很高的收入。所以我没有很高的收入。”试指明前提和结论，试指明前提和结论，并给予证明。并给予证明。n课堂实训课堂实训. 武汉大学国际软件学院唐存琛 刘峰34应用实例应用实例2 将下列条件作为前提，验证所得结论是将下列条件作为前提，验证所得结论是否有效：否有效：(a) 明天或是天晴，或是下雨；明天或是天晴，或是下雨；(b) 如果是天晴，我去公园；如果是天晴，我去公园；(c) 如果我去公园，我就不看书。如果我去公园，我就不看书。结论：如果我在看书，则天下雨。结论：如果我在看书，则天下雨。. 武

19、汉大学国际软件学院唐存琛 刘峰35三、公理系统三、公理系统1、公理系统的组成、公理系统的组成（1）初始符号：）初始符号：它们是不经定义而直接使用的符号；它们是不经定义而直接使用的符号；（2）形成规则：）形成规则：确定定义在初始符号上的哪些符号串确定定义在初始符号上的哪些符号串是合式公式；是合式公式；（3）公理集：）公理集：它们是不经证明而直接认为是恒真的命它们是不经证明而直接认为是恒真的命题；题；（4）推理规则：）推理规则：规定如何从公理和前面已推导出的合规定如何从公理和前面已推导出的合式公式经过符号变形而推出其它公式。式公式经过符号变形而推出其它公式。. 武汉大学国际软件学院唐存琛 刘峰36

20、2、公理系统、公理系统L12,()ippp 公理系统公理系统L的定义：的定义：1、初始符号：、初始符号：2、形成规则：、形成规则：(1)(2)(3)(4)ipAAABAB（1in)是合式公式;若 是合式公式,则()是合式公式;若 和 是合式公式,则()是合式公式;只有通过有限次使用(1) (3)得到的符号串才是合式公式。. 武汉大学国际软件学院唐存琛 刘峰373、公理集：、公理集：123()()()()()()()()()()LABALABCABACLABBA 4、推理规则：假言推理规则（、推理规则：假言推理规则（MP规则）。规则）。. 武汉大学国际软件学院唐存琛 刘峰38L证证L2L1(1)、(2)，MPL1(1)、(2)，MPL1(3)、(4)，MPL2)()(1121PPPP)()()()()()()()()(11211211121121321PPPPPPPPPPPPPP例例9 证明证明L2L1MP规则规则. 武汉大学国际软件学院唐存琛 刘峰39证证LAAAAAAAAAAAAAAAA