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

1、. 武汉大学国际软件学院唐存琛 刘峰,1,2.4 命题逻辑推理理论,2.4.1 推理的形式结构 推理及其形式结构 推理定律 2.4.2 自然推理系统P 自然推理系统的定义 证明方法,. 武汉大学国际软件学院唐存琛 刘峰,2,2.4.1 推理的形式结构,一、什么是推理,定义2.19 设A1，A2 ， ，Ak ，B都是命题公式，若对于每组赋值, A1A2 Ak为假, 或者当A1 A2 Ak为真时，B也为真, 则称由前提A1，A2，, Ak推B的推理有效或推理正确, 并称B是有效的结论。,. 武汉大学国际软件学院唐存琛 刘峰,3,定理2.8 由前提A1, A2, , Ak 推出B 的推理正确当且仅当

2、 A1 A2 Ak B为重言式.,如果把（A1 A2 Ak ） B为永真式记为：,上式的含义？,. 武汉大学国际软件学院唐存琛 刘峰,4,二、推理的形式结构,定义2.20 称（A1 A2 Ak ） B为由前提 A1, A2, , Ak推结论 B 的推理的形式结构。,推理的形式结构一般有以下三种： 形式(1) A1 A2 Ak B 形式(2) 前提: A1, A2, , Ak 结论: B 形式(3) A1， A2 ， ， Ak B,. 武汉大学国际软件学院唐存琛 刘峰,5,真值表法 等值演算法 主析取范式法 构造证明法,判断推理是否正确的方法:,真值表的方法参见P.67例2.23。,. 武汉大学

3、国际软件学院唐存琛 刘峰,6,例1 判断下面推理是否正确: (1) 若今天是1号, 则明天是5号. 今天是1号. 所以, 明天是5号.,. 武汉大学国际软件学院唐存琛 刘峰,7,例1 (2) 若今天是1号, 则明天是5号. 明天是5号. 所以, 今天是1号。,解 设 p: 今天是1号, q: 明天是5号 推理的形式结构为 证明 用主析取范式法,这不是一个永真式，01是该公式成假的赋值，所以推理不正确。,. 武汉大学国际软件学院唐存琛 刘峰,8,三、推理规则 1、推理规则的定义,是一个推理规则，当且仅当 ，其中, A1, A2, , An 称为推理规则的前提，B 称为推理规则的结论。,. 武汉大

4、学国际软件学院唐存琛 刘峰,9,1）附加规则,2）化简规则,3）MP规则 （假言推理）,4）拒取式,2、常用的推理规则,. 武汉大学国际软件学院唐存琛 刘峰,10,5）析取三段论,6）假言三段论,7）合取引入,8）构造性二难,2、常见的推理规则（续）,. 武汉大学国际软件学院唐存琛 刘峰,11,注意：,（1）推理规则中出现的A、B、C 等是元语言符号； （2）直接引用而不需证明，只要说明所引用规则的名称； （3）24个永真公式每个都可以等效为2个推理规则。,. 武汉大学国际软件学院唐存琛 刘峰,12,2.4.2 自然推理系统P,自然推理系统P由下述3部分组成: 1. 字母表 (1) 命题变项符

5、号: p,q,r, pi,qi,ri, (2) 联结词: , , , , (3) 括号与逗号: ( ), , 2. 合式公式,一、自然推理系统P的定义,. 武汉大学国际软件学院唐存琛 刘峰,13,3. 推理规则 (1) 前提引入规则 (2) 结论引入规则 (3) 置换规则 (4) 假言推理规则 (5) 附加规则 (6) 化简规则,一、自然推理系统P的定义（续）,(7) 拒取式规则 (8) 假言三段论规则 (9) 析取三段论规则 (10)构造性二难推理规则 (11) 破坏性二难推理规则 (12) 合取引入规则,. 武汉大学国际软件学院唐存琛 刘峰,14,证,例2 证明,. 武汉大学国际软件学院唐

6、存琛 刘峰,15,二、证明方法,用推理的概念说明一些证明方法的正确性。,为了证明 ，只需证明 A 永假即可。,（2）后件真证明法,为了证明 ，只需证明 B 永真即可。,（1）前件假证明法,. 武汉大学国际软件学院唐存琛 刘峰,16,（3）直接证明法,为了证明 ，只需证明若 A 为真，则 B 亦为真。,为了证明 ，只需证明若 B 为假，则 A 亦为假。,（4）间接证明法,. 武汉大学国际软件学院唐存琛 刘峰,17,（5）分情况证明法,只需证明对任意的 ，均有 。,为了证明 ,（6）附加前提证明法,只需证明,为了证明 ,. 武汉大学国际软件学院唐存琛 刘峰,18,附加前提证明法的说明：,理由: (

7、A1A2Ak)(CB) ( A1A2Ak)(CB) ( A1A2AkC)B (A1A2AkC)B,欲证明 等价地证明 前提: A1, A2, , Ak 前提: A1, A2, , Ak, C 结论: CB 结论: B,. 武汉大学国际软件学院唐存琛 刘峰,19,不相容的概念：,定义 若 是可满足式，则称公式集 是相容的（或一致的），否则，称之为不相容的。,. 武汉大学国际软件学院唐存琛 刘峰,20,（7）反证法（归谬法）,为了证明,. 武汉大学国际软件学院唐存琛 刘峰,21,归谬法(反证法)的说明,理由: A1A2AkB (A1A2Ak)B (A1A2AkB) 括号内部为矛盾式当且仅当 (A1

8、A2AkB)为重言式,欲证明 前提：A1, A2, , Ak 结论：B 将B加入前提, 若推出矛盾, 则得证推理正确.,. 武汉大学国际软件学院唐存琛 刘峰,22,证,例3 证明,前提 附加前提 、，假言推理 前提 、，拒取式 、，析取三段论 前提 、，拒取式 、，CP, ,. 武汉大学国际软件学院唐存琛 刘峰,23,证,例4 证明,. 武汉大学国际软件学院唐存琛 刘峰,24,直接证明法举例,例5 在自然推理系统P中构造下面推理的证明: 前提: 结论: 证明：,前提 前提 (1)、(2)拒取式 前提 (3)、(4)析取三段论,. 武汉大学国际软件学院唐存琛 刘峰,25,前提 (5)、(6)假言

9、推理 (7)、(4)合取,. 武汉大学国际软件学院唐存琛 刘峰,26,例6 构造推理的证明: 若明天是星期一或星期三, 我就有课. 若有课, 今天必需备课. 我今天下午没备课. 所以, 明天不是星期一和星期三.,解 设 p:明天是星期一, q:明天是星期三， r:我有课， s:我备课 前提: (pq)r, rs, s 结论: pq,. 武汉大学国际软件学院唐存琛 刘峰,27,前提: (pq)r, rs, s 结论: pq 证明： rs 前提引入 s 前提引入 r 拒取式 (pq)r 前提引入 (pq) 拒取式 pq 置换 结论有效, 即明天不是星期一和星期三.,. 武汉大学国际软件学院唐存琛

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

11、学院唐存琛 刘峰,31,例8 构造下面推理的证明 前提: (pq)r, rs, s, p ；结论: q,证明：用归缪法 q 结论否定引入 rs 前提引入 s 前提引入 r 拒取式 (pq)r 前提引入 (pq) 析取三段论 pq 置换 p 析取三段论,. 武汉大学国际软件学院唐存琛 刘峰,32, p 前提引入 pp 合取 推理正确, q是有效结论,. 武汉大学国际软件学院唐存琛 刘峰,33,应用实例1 分析下列事实“如果我有很高的收入，那么我就能资助许多贫困学生；如果我能资助许多贫困学生，那么我很高兴；但我不高兴，所以我没有很高的收入。”试指明前提和结论，并给予证明。,课堂实训,. 武汉大学国

12、际软件学院唐存琛 刘峰,34,应用实例2 将下列条件作为前提，验证所得结论是否有效： 明天或是天晴，或是下雨； 如果是天晴，我去公园； 如果我去公园，我就不看书。 结论：如果我在看书，则天下雨。,. 武汉大学国际软件学院唐存琛 刘峰,35,三、公理系统 1、公理系统的组成,（1）初始符号：它们是不经定义而直接使用的符号； （2）形成规则：确定定义在初始符号上的哪些符号串是合式公式； （3）公理集：它们是不经证明而直接认为是恒真的命题； （4）推理规则：规定如何从公理和前面已推导出的合式公式经过符号变形而推出其它公式。,. 武汉大学国际软件学院唐存琛 刘峰,36,2、公理系统L,公理系统L的定义

13、： 1、初始符号：,2、形成规则：,. 武汉大学国际软件学院唐存琛 刘峰,37,3、公理集：,4、推理规则：假言推理规则（MP规则）。,. 武汉大学国际软件学院唐存琛 刘峰,38,L,证,L2 L1 (1)、(2)，MP,L1 (1)、(2)，MP L1 (3)、(4)，MP,L2,例9 证明,L2 L1 MP规则,. 武汉大学国际软件学院唐存琛 刘峰,39,证,L,例10 证明,. 武汉大学国际软件学院唐存琛 刘峰,40,3、演绎定理,例11 证明,证,假设 L2 (1)、(2)，MP L1 假设 (4)、(5)，MP (3)、(6)，MP,L,. 武汉大学国际软件学院唐存琛 刘峰,41,L的演绎定理：若,L,，则,L,。,推论：设A，B和C是L的任意合式公式，则,L,。,例12 证明 L,证,L1 L3 (1)、(2)，HS,. 武