国防科学技术大学:《数理逻辑》(英文版)Lecture 4 Propositional Calculus(Cont’d)

Logic in Computer Science An Introductory Course for Master Students Wang j iwang@nudt.edu.cn ecture Propositional Calculus( Cont'd) Logic in Computer Science- p 1/19
Logic in Computer Science An Introductory Course for Master Students Wang Ji jiwang@nudt.edu.cn Lecture 4 Propositional Calculus(Cont’d) Logic in Computer Science – p.1/19

PROPOSITIONAL CONNECTIVES Logic in Computer Science- p 2/19
Propositional Connectives Logic in Computer Science – p.2/19

Substitutivity of equivalence Let A, m and n be wffs and let an be the result replacing M by N at zero or more occurrences Henceforth called designate occurrences) of M in A 1. AN is a wff 2. IfFM=N then FA=An If H M=n then F A=An Logic in Computer Science -p 3/19
Substitutivity of Equivalence Let A,M and N be wffs and let AMN be the result of replacing M by N at zero or more occurrences (henceforth called designate occurrences) of M in A. 1. AMN is a wff. 2. If |= M ≡ N then |= A ≡ AMN . (≡ sub) If ` M ≡ N then ` A ≡ AMN Logic in Computer Science – p.3/19

Propositional connectives An n-ary truth function is a function from ples of truth values to truth values n-tuples A propositional connective is a symbol of a formalized language which in the intend interpretation, denotes a truth function How to lift a wff to be a truth function? Logic in Computer Science -p 4/19
Propositional Connectives • An n-ary truth function is a function from n-tuples of truth values to truth values. • A propositional connective is a symbol of a formalized language which, in the intend interpretation, denotes a truth function. • How to lift a wff to be a truth function? Logic in Computer Science – p.4/19

入 Abstraction If p1,... Pn are distinct propositional variables including all variables in A, let Ap1…入pn]A:{T,F}→{T,F} where 1 n)=0(A) and(p)=;forl0≤i≤m Obviously.Ap1…入pA=Ap1… n B iff A≡B Logic in Computer Science-p.5/19
λ Abstraction If p1, · · · , pn are distinct propositional variables including all variables in A, let [λp1 · · · λpn]A : {T, F}n → {T, F} where [λp1 · · · λpn]A(x1, · · · , xn) = φ(A) and φ(pi) = xi for all 0 ≤ i ≤ n. Obviously, [λp1 · · · λpn]A = [λp1 · · · λpn]B iff A ≡ B Logic in Computer Science – p.5/19

Normal form A literal is a wff of the form p or of the form a p a wff is in disjunctive normal form iff it is a disjunction of conjunctions of literals m70 ∨∧ A wff is in conjunctive normal form iff it is a conjunction of disjunctions of literals p Logic in Computer Science -p6/19
Normal Form • A literal is a wff of the form p or of the form ∼ p • A wff is in disjunctive normal form iff it is a disjunction of conjunctions of literals. _ m i=1 ^ ni j=1 pij • A wff is in conjunctive normal form iff it is a conjunction of disjunctions of literals. ^ m i=1 _ ni j=1 pij Logic in Computer Science – p.6/19

Disjunctive Normal Form Theorem 1. Let h be any truth function with n arguments where n>l, and let p1, ...,pn be distinct propositional variables. Then there is a wff a in disjunctive normal form such that h=Ap1…入nA 2. For every wff b of propositional calculus there is a wff a in disjunctive normal form such that b is equivalent A Logic in Computer Science-p. 7/19
Disjunctive Normal Form Theorem 1. Let h be any truth function with n arguments, where n ≥ 1, and let p1, · · · , pn be distinct propositional variables. Then there is a wff A in disjunctive normal form such that h = [λp1 · · · λpn]A. 2. For every wff B of propositional calculus there is a wff A in disjunctive normal form such that B is equivalent A. Logic in Computer Science – p.7/19

Completeness of Propositional Connectives A set T of propositional connectives is complete iff for each integer m> l and for each truth function h of n arguments there is a wff a in which only connectives of f occur such that h=DAp1…~pA iN,vi is complete Logic in Computer Science -p8/19
Completeness of Propositional Connectives • A set Υ of propositional connectives is complete iff for each integer n ≥ 1 and for each truth function h of n arguments, there is a wff A in which only connectives of Υ occur such that h = [λp1 · · · λpn]A • {∼,∨} is complete. Logic in Computer Science – p.8/19

Negation Normal Form A wff of propositional calculus is in negation normal form iff it contains no propositional connectives other than∧,∨Vand~, and the scope ot each occurrence ot N is a propositional variable Get nne get rid of≡and, leaving just∧,∨and 2. push negations in, using law of double negation and de le Morgan s law (AVB)≡~A∧~B (A∧B) A∨~B Logic in Computer Science-p.9/19
Negation Normal Form • A wff of propositional calculus is in negation normal form iff it contains no propositional connectives other than ∧, ∨ and ∼, and the scope of each occurrence of ∼ is a propositional variable. • Get NNF 1. get rid of ≡ and ⊃, leaving just ∧, ∨ and ∼ 2. push negations in, using law of double negation and de Morgan’s law ∼∼ A ≡ A ∼ (A ∨ B) ≡ ∼ A∧ ∼ B ∼ (A ∧ B) ≡ ∼ A∨ ∼ B Logic in Computer Science – p.9/19

Conjuncts of NNF For each wff A in negation normal form define a set C(A)of conjuncts of A by induction as follows If A is a literal, C(A=AJ If a has the form bVC, C(A=C(BUC(C If a has the form b∧C, CA)={D∧ED∈C(B)andE∈C(C Logic in Computer Science- p10/19
Conjuncts of NNF For each wff A in negation normal form, define a set C(A) of conjuncts of A by induction as follows • If A is a literal, C(A) = {A} • If A has the form B ∨ C, C(A) = C(B) ∪ C(C) • If A has the form B ∧ C, C(A) = {D ∧ E|D ∈ C(B) and E ∈ C(C)} Logic in Computer Science – p.10/19
按次数下载不扣除下载券;
注册用户24小时内重复下载只扣除一次;
顺序:VIP每日次数-->可用次数-->下载券;
- 国防科学技术大学:《数理逻辑》(英文版)Lecture 3 Propositional Calculus(Cont’d).pdf
- 国防科学技术大学:《数理逻辑》(英文版)Lecture 2 Propositional Calculus.pdf
- 国防科学技术大学:《数理逻辑》(英文版)Lecture 1 Preliminaries.pdf
- 国防科学技术大学:《数理逻辑》课程考试模拟试卷.pdf
- 金陵学院:《计算机应用》课程教学资源(PPT课件)第六章 Matlab程序.ppt
- 金陵学院:《计算机应用》课程教学资源(PPT课件)第五章 Matlab绘图.ppt
- 金陵学院:《计算机应用》课程教学资源(PPT课件)第四章 数据类型和输入输出.ppt
- 金陵学院:《计算机应用》课程教学资源(PPT课件)第三章 矩阵和Matlab(主讲:袁杰).ppt
- 金陵学院:《计算机应用》课程教学资源(PPT课件)第二章 Matlab基本知识.ppt
- 《Visual Basic6.0程序设计》绪论.ppt
- 《Visual Basic6.0程序设计》第五章 对话框与菜单.ppt
- 《Visual Basic 6.0程序设计》课程电子教案(PPT教学课件)第四章 窗体及常用控件.ppt
- 《Visual Basic 6.0程序设计》课程电子教案(PPT教学课件)第三章 VB语言程序设计基础.ppt
- 《Visual Basic 6.0程序设计》课程电子教案(PPT教学课件)第三章 VB语言程序设计基础.ppt
- 《Visual Basic 6.0程序设计》课程电子教案(PPT教学课件)第六章 过程、模块与类.ppt
- 《Visual Basic 6.0程序设计》课程电子教案(PPT教学课件)第二章 中文Visual Basic(VB)6.0概述.ppt
- 《Visual Basic 6.0程序设计》课程电子教案(PPT教学课件)第五章 对话框与菜单.ppt
- 《Visual Basic 6.0程序设计》课程电子教案(PPT教学课件)第七章 常用算法.ppt
- 《Visual Basic 6.0程序设计》课程电子教案(PPT教学课件)第一章 程序设计概述.ppt
- 万博科技职业学院:《Visual Basic程序设计》讲义.ppt
- 国防科学技术大学:《数理逻辑》(英文版)Lecture 5 Predicate Calculus.pdf
- 国防科学技术大学:《数理逻辑》(英文版)Lecture 6 Reasoning in Predicate Calculus.pdf
- 国防科学技术大学:《数理逻辑》(英文版)Lecture 7 Prenex Normal Form.pdf
- 国防科学技术大学:《数理逻辑》(英文版)Lecture 8 Semantics.pdf
- 国防科学技术大学:《数理逻辑》(英文版)Lecture 9 Independence.pdf
- 国防科学技术大学:《数理逻辑》(英文版)Lecture 10 Completenss.pdf
- 国防科学技术大学:《数理逻辑》(英文版)Lecture 11 Syntax.pdf
- 《计算机网络管理与安全技术》课程教学资源(PPT课件)第7章 防火墙(李艇).ppt
- 《计算机网络管理与安全技术》课程教学资源(PPT课件)第1章 网络管理概述(李艇).ppt
- 《计算机网络管理与安全技术》课程教学资源(PPT课件)第2章 管理信息结构与管理信息库(李艇).ppt
- 《计算机网络管理与安全技术》课程教学资源(PPT课件)第3章 SNMP通信模型与RMON规范(李艇).ppt
- 《计算机网络管理与安全技术》课程教学资源(PPT课件)第4章 网络管理系统(李艇).ppt
- 《计算机网络管理与安全技术》课程教学资源(PPT课件)第5章 网络安全基础(李艇).ppt
- 《计算机网络管理与安全技术》课程教学资源(PPT课件)第6章 网络安全技术(李艇).ppt
- 清华大学:《文献检索》Practice1_work.doc
- 清华大学:《文献检索》课程教学资源(PPT课件)1、检索基础知识.ppt
- 清华大学:《文献检索》课程教学资源(PPT课件)2、计算机信息检索.ppt
- 清华大学:《文献检索》课程教学资源(PPT课件)3、计算机检索方法(Ei_Web).ppt
- 清华大学:《文献检索》课程教学资源(PPT课件)4、计算机检索方法(SCI_Web).ppt
- 清华大学:《文献检索》课程教学资源(PPT课件)5、学术资源的利用(孙平).ppt