命题逻辑自然演绎系统课件_第1页
命题逻辑自然演绎系统课件_第2页
命题逻辑自然演绎系统课件_第3页
命题逻辑自然演绎系统课件_第4页
命题逻辑自然演绎系统课件_第5页
已阅读5页,还剩50页未读 继续免费阅读

下载本文档

版权说明:本文档由用户提供并上传,收益归属内容提供方,若内容存在侵权,请进行举报或认领

文档简介

1、 第四章 命题逻辑的自然演绎系统自然演绎系统NP命题逻辑的自然演绎系统NP是由形式语言L 和一组推导(变形)规则构成的。其中形式语言L 包括初始符号、形成规则和定义。 构建命题逻辑的形式系统,可以采用公理化方法,也可采用自然演绎的方法。为接近人们日常思维的实践,采用自然演绎的方法来构建命题逻辑的一个形式系统NP。7/16/20222初始符号(1)甲类符号:p1, p2, p3, ;(2)乙类符号:,;(3)丙类符号:(,)。这些符号构成的有穷长的序列叫做符号串,例如:p, pq,pq, pq;(pq)r,p(qr),;(pqpq),(pqr), 按照形成规则形成的符号串称为合式公式。7/16/

2、20223形成规则(1)任何单个的命题变元p是合式公式;(2)如果A是合式公式,则(A)是合式公式;(3)如果A和B是合式公式,则(AB)、(AB)、(AB)是合式公式;只有(1)-到(3)形成的符号串是合式公式。7/16/20224定义定义是用来表示缩写的,定义两边的符号串可以相互代替。如:(AB)=df(AB)(BA)。形式语言L 的全体合式公式记为Form(L )。形式语言L 是我们研究对象,叫对象语言。讨论对象语言的语言叫元语言或语法语言。7/16/20225形成规则的作用(1)以递归的方式定义合式公式。(2)提供一种能行、可判定的方法判定任一符号串是不是合式公式。(3)检验合式公式的

3、性质。如:(pq)(p)q)的形成过程是:p,q,(pq),(p),(pq)(p),q ,(pq)(p)q)。这个字符串是反复运用形成规则而形成的,因此它是合式公式。7/16/20226合式公式的子公式合式公式的子公式:在生成合式公式的过程中,每一步所生成的公式都是这一生成的合式公式的子公式。如: A的子公式是A和A; AB 的子公式是A、B和AB; AB 的子公式是A、B和AB; AB 的子公式是A、B和AB。如:p,q,(pq),(p),(pq)(p),(pq)(p)q)都是(pq)(p)q)的子公式。主联结词:辖域最大的联结词。(pq)(p)q)的主联结词是。省略括号的约定:(1)公式最

4、外层的括号可以省略。(2)联结词的结合力依下列次序递减:,。如:(pq)(p)q)可简记为(pq)pq。7/16/20227推演规则(1)整推规则(2)置换规则(3)条件证明规则(4)间接证明规则7/16/20228整推规则1.合取引入规则(记为+): 从A和B推出AB;2.合取消去规则(记为_): 从AB推出A;从AB推出B;3.析取引入规则(记为+): 从A推出AB;从B推出AB;4.析取消去规则(记为_): 从AB和A推出B;从AB和B推出A;5.肯定前件(记为MP) 从AB和A推出B;6.否定后件规则(记为MT); 从AB和B推出A;7/16/20229条件证明规则5.蕴涵引入规则(记

5、为+): 条件证明 如果从公式集和A推出B,则从推出AB;7/16/202210例1: R(HT) RH TS H HS R(HT) 前提 RH 前提 TS 前提 H 前提 R 否后 HT 肯前 HS 假言三段论7/16/202211例2:BA B(CD) AC D BA BA 前提 B(CD) 前提 AC 前提 B 化简 CD 化简 A 肯前 C 否析 D 肯前7/16/202212例3:FG(H(IK) HI HMF IK FG(H(IK) 前提 HI 前提 HMF 前提 H 化简 HM 附加 F 肯前 FG 附加 H(IK) 肯前 IK 肯前7/16/202213练习:1. M(NL)

6、JK M M(NJ) LK 7/16/202214 M(NL) 前提 JK 前提 M 前提 M(NJ) 前提 NL 肯前 NJ 否析 LK 二难推理7/16/2022152. P(RQ) PQ SRQ S R 7/16/202216 P(RQ) 前提 PQ 前提 SRQ 前提 S 前提 SR 附加 Q 肯前 P 否后 RQ 肯前 R 否后7/16/2022173. PQ(RS) P (RS)(TU) U T 7/16/202218 PQ(RS) 前提 P 前提 (RS)(TU) 前提 U 前提 PQ 附加 (RS) 肯前 TU 否析 T 否后7/16/202219条件证明规则 步 骤: 1.引

7、入假设 2.撤销假设 (适用于蕴含式)7/16/202220蕴涵引入规则(记为+) 又称条件证明规则或演绎定理,是把从推出AB的推理转化为从和临时的假设A推出B的推理。即:(AB)(AB) 本规则实质就是条件输入(输出)规则的运用 最适于证明结论为蕴涵式的推论。 前提集结论假设前提7/16/202221蕴涵引入规则(记为+)例1:FG HF GH FG 前提 HF 前提 G 条件假设 G 双重否定 F 否析律 F 双重否定 H 否后律 H 双重否定 GH 条件证明7/16/202222蕴涵引入规则(记为+)例2:AB CB(DE) A(DE) AB 前提 CB(DE) 前提 A 条件假设 B

8、肯前律 CB 附加 DE 肯前律 A(DE) 条件证明7/16/202223间接证明规则 否定消去规则(记为_): 间接证明 如果从和A推出BB,则从推出A。 步骤: 1.否定结论 2.提出矛盾 3.肯定结论7/16/202224否定消去规则(记为_) 又称间接证明或反证法,是把由推出A的推理转化为由和临时的假设A推出BB的推理。 最适于证明结论不是蕴涵式的推论。7/16/202225否定消去规则(记为_)例1:AB AB A(1) AB 前提(2) AB 前提 (3) A 间接假设 (4) A (3),_ (5) B (1),(4),_ (6) B (2),(4),_ (7) BB (5),

9、(6),+(8) A (3)(7),间接证明7/16/202226否定消去规则(记为_)例2:A(BC)(CD),CD / A(1) A(BC) (CD) A1(2)CD A2(3) C (2)_ (4) D (2)_ (5) A H1 (6) A (5)_ (7) (BC)(CD) (1),(6)_ (8) CD (7)_ (9) D (3),(8)_ (10) DD (4),(9)+(11)A (5)(10)- (消去H1) 7/16/202227蕴涵引入(条件证明)规则与 否定消去(间接证明)规则在做题过程中二者可以交替使用,既可以先用蕴涵引入(条件证明)规则再用否定消去(间接证明)规则

10、,也可以先用否定消去(间接证明)规则再用蕴涵引入(条件证明)规则。7/16/202228练习1、XYZ ZX XY 7/16/202229 XYZ 前提 ZX 前提 X 条件假设 YZ 肯前律 X 双重否定 Z 否后率 Y 否析律 XY 条件证明7/16/202230练习:2. E(JK) J(KE) E7/16/202231 E(JK) 前提 J(KE) 前提 E 间接假设 JK 否析律 J 化简 KE 肯前律 E 化简 EE 合取 E 间接证明7/16/202232作业:1. XY XZ ZW YW 2. EFG EH IK FJI K 7/16/2022333. FG HF GH4. E

11、(JK) J(KE) E7/16/202234置换规则的涵义 对于任何命题P,无论它是以整个命题出现,还是作为一个命题的一部分出现,都可用与它重言等值的命题Q来替换。7/16/202235置换规则T18(a) (AB)A B(记为DeM.)T18(b) (AB)A B(记为DeM.)7/16/202236德摩根律的证明T18(a) (AB) A B的证明先证(AB) AB:(1) (AB) A (2) (AB) H1 (3) A H2 (4) AB (3),+ (5)(AB)(AB) (2),(4),+ (6) A (3)(5),_(消去H2) (7) B H3 (8)AB (7),+ (9)

12、(AB)(AB) (2),(8),+ (10) B (7)(9),_(消去H3) (11)AB (6),(10), + (12)(AB)(AB) (1),(11), +(13) AB (2)(12),_(消去H1)7/16/202237德摩根律的证明T18(a) (AB) A B的证明再证AB (AB):(1) AB A (2) (AB) H (3) AB (2),_ (4) A (3),_ (5) B (3),_ (6) A (4),+(7) B (1),(6),_ (8)BB (5),(7),+(9)(AB) (2)(8),_(消去H)7/16/202238置换规则交换律T21(a) AB

13、BAT21(b) ABBA结合律T22(a) A(BC)(AB)CT22(b) A(BC)(AB)C7/16/202239置换规则分配律T23(a) A(BC)(AB)(AC)T23(b) A(BC)(AB)(AC)蕴析律(A B) (AB)德 摩 根 律(AB) (A B)(AB) (AB) 7/16/202240置换规则的证明T21(b) ABBA的证明先证AB BA(1) AB A (2) A H1 (3) BA (2),+ (4) ABA (2)(3),+(消去H1) (5) B H2 (6) BA (5),+(7) BBA (5)(6),+(消去H2)(8) BA (1),(4),(

14、7),D.C.同理,可证BAAB。7/16/202241NP系统中的语法(语形)推出关系T24(a) (B)AB T24(b) AB(AB) T25(a) ABAB (蕴析律)T25(b) ABAT26(a) (AB)AT26(b) A(A)T27(a) A(A)T27(b) A(A)T28(b) AB,AC,BCA(二难推理)T28(c) AC,BD,ABCDT28(d) AC,BD,CDAB7/16/202242NP系统中的语法(语形)推出关系T29(a) ABCACB(反三段论)T29(b) ABCBCAT30 ABC A(BC)(条件输出)T31 A(BC) ABC(条件输入)T32

15、A(BC)B(AC)(条件互易)T33 A(BC)(AB)(AC)(蕴涵分配) T34 A(AB)AB (条件融合)T35(a) AB ACBC (前件附加)T35(b) AB ACBCT35(c) AB (CA)(CB)T36 (AB)C BC 7/16/202243NP系统中的语法(语形)推出关系T37 AB,BA AB (+)T38(a) AB AB (_)T38(b) AB BAT39 AC,BC ABC (前件合取) T40 AB,AC ABC (后件合取) T41 ABC(AC)(BC)T42 ABC(AC)(BC)T43 ABC(AB)(AC)T44 ABC(AB)(AC)7/1

16、6/202244NP系统中的语法(语形)推出关系应用实例(一)如果不换8号上场(p)或者12号上场(q),甲队的形势不会好转(r)。教练没有换8号上场,也没有换12号上场。所以,甲队的形势不会好转。首先,将前提和结论形式化: A1:(pq)r A2:pq B:r(1) (pq)r A1(2) pq A2(3) (pq) (2),DeM.(4) r (1),(3),_7/16/202245NP系统中的语法(语形)推出关系应用实例(二)如果线段L有存在无穷多个点,那么,如果这些点有长度,则线段L将无穷长,而且,如果这些点都没有长度,则线段L也不会有长度。但是,一条线段既不会无穷长,也不会没有长度。

17、所以L上不会有无穷多个点。前题和结论符号化:A1:p(qr)(qs)A2:rsB:p7/16/202246(1) p(qr)(qs) A1(2) rs A2 (3) p H (4) p (3), _ (5) (qr)(qs) (1),(4),_ (6) qr (5),_ (7) qs (5),_ (8) r (2),_ (9) s (2),_ (10) q (6),(8), M.T. (11) q (7),(9), M.T. (12) qq (10),(11),+(13) p (3)(12),_,(消去H)7/16/202247NP系统中的语法(语形)推出关系应用实例(三)如果货币供应量保持现

18、状,而货币需求量增加,则银行利率就会上升。如果货币需求量增加导致银行利率上升,则在银行存款更被看好。主管部门已宣布货币供应总是保持不变。因此,在银行存款更被看好。A1:pqrA2:(qr)sA3: pB: s7/16/202248NP系统中的语法(语形)推出关系应用实例(三)方法一:(1) pqr A1(2)(qr)s A2(3) p A3 (4) q H1 (5) pq (3),(4),+ (6) r (1),(5),_(7)qr (4)(6),+(消去H1)(8)s (2),(7),_7/16/202249NP系统中的语法(语形)推出关系应用实例(三)方法二:(1) pqr A1(2)(qr)s A2(3)

温馨提示

  • 1. 本站所有资源如无特殊说明,都需要本地电脑安装OFFICE2007和PDF阅读器。图纸软件为CAD,CAXA,PROE,UG,SolidWorks等.压缩文件请下载最新的WinRAR软件解压。
  • 2. 本站的文档不包含任何第三方提供的附件图纸等,如果需要附件,请联系上传者。文件的所有权益归上传用户所有。
  • 3. 本站RAR压缩包中若带图纸,网页内容里面会有图纸预览,若没有图纸预览就没有图纸。
  • 4. 未经权益所有人同意不得将文件中的内容挪作商业或盈利用途。
  • 5. 人人文库网仅提供信息存储空间,仅对用户上传内容的表现方式做保护处理,对用户上传分享的文档内容本身不做任何修改或编辑,并不能对任何下载内容负责。
  • 6. 下载文件中如有侵权或不适当内容,请与我们联系,我们立即纠正。
  • 7. 本站不保证下载资源的准确性、安全性和完整性, 同时也不承担用户因使用这些下载资源对自己和他人造成任何形式的伤害或损失。

评论

0/150

提交评论