《数理逻辑》全册配套课件.ppt

1、 超级计算学院 数理逻辑 第 0 章 introduction数理逻辑全册配套课件数理逻辑全册配套课件 超级计算学院 数理逻辑 第 0 章 introductionMathematic Logic In Computer Science 超级计算学院 数理逻辑 第 0 章 introductionThe brief introduction toMathematic Logic In Computer Science 超级计算学院 数理逻辑 第 0 章 introduction1. Propositional logic2. Predicate logic3. Resolution metho

2、d4. Applications of logic in computer science5. Verification by model check6. Program verification7. Modal logic and agent 超级计算学院 数理逻辑 第 0 章 introductionThe motivations of leaning the courseLogic , a science is to research how to reason 1. Make men wise 2. Use computer to reason 3. It is the base of

3、 multiple computer fields such as AI, Database. Software engineering computer languages 4. It can help us analyze problems, describe problems and solve problems, do the research work. 超级计算学院 数理逻辑 第 0 章 introductionHow to learn the course 1. Come to listen to lessons. Logic is difficult to understand

4、, If you do not take the lessons, you may spend the more time to read textbook. You do not know what is important, that I highlight, and what is less important, I introduce the final results only. Not give proof in detail. Some contents are newly added. 2. Think. It is important to understand the co

5、ntents of the course, not recite the definition. 3. Do homework. 超级计算学院 数理逻辑 第 0 章 introductionScore and evaluation1. Q and A, Discussion, Test , 30%2. Term examination, 70% 超级计算学院 数理逻辑 第 0 章 introductionReference book1.Logic in Computer Science (Second Edition) (英) Michael Huth (伦敦帝国学院) 2. Principl

6、es of Artificial Intelligence (美) Nilsson, N.J. 1980(斯坦福大学) 超级计算学院 数理逻辑 第 0 章 introductionThank YouThe end of Chapter 0 超级计算学院 数理逻辑 第 0 章 introductionChapter 1 Propositional Logic 超级计算学院 数理逻辑 第 0 章 introduction1.3 propositional logic as a formal language(page 31)Proposition and propositional atomDef

7、inition 1.27 The well-formed formula of propositional logic are those, which we obtain by using the construction rulers below, and only those finitely many time: 超级计算学院 数理逻辑 第 0 章 introductionAtomic: Every propositional atom p, q, r,. and p1, p2, p3 ,is a well-formed formula: if is a a well-formed f

8、ormula, then so ( ): if and are well-formed formula, then so ( ): if and are well-formed formula, then so ( ): if and are well-formed formula, then so ( ) 超级计算学院 数理逻辑 第 0 章 introductionBackus Naur form(BNF):=p| () | () | () |() Example: (p) q) (p(q (r) 超级计算学院 数理逻辑 第 0 章 introductionr qppq A Parse tr

9、ee 超级计算学院 数理逻辑 第 0 章 introduction1.4 semantics of propositional logic (page 36) TheTruth Table for logic connectivesPQ100 00P010 11 01 10010 010 11 01 1110P Q0 010 11 01 1101P Q 超级计算学院 数理逻辑 第 0 章 introductionDefinition: (Interpretation s for a formula and its value under the interpretation)Definitio

10、n: (Formula equivalence) If for any interpretation P, Q have same truth value. Denoted by P Q 超级计算学院 数理逻辑 第 0 章 introductionEquivalent formulas1. P P2. P Q Q P QPQPQPQP)()()(RQPRQP)()()(RPQPRQPQPQP)()()(RQPRQP)()()(RPQPRQP8.5.4.3.7.6. 超级计算学院 数理逻辑 第 0 章 introductionDefinition: (Formula implication re

11、lation)Let I be an interpretation for formulas P and Q, if I make P true, then I make Q true, We say that P implies Q, write as P = QNote: We should pay attention the difference between = and 超级计算学院 数理逻辑 第 0 章 introduction Basic implication rulers. (1) (2) (3) (4) (5) (6) (7) (8),ABA.BBA.,BABBAA.,BA

12、BA.,BABA.,BABA.,ABBA.,CACBBA.,CCBCABA 超级计算学院 数理逻辑 第 0 章 introductionRuler set for Natural Deduction: All equivalence formula +all implication rulers.Natural DeductionDefinition : deductionLet S=1, 2, , n be a set of formulas, be a formula(S is called premise set, consequence ),Do the below steps, ge

13、tting a sequence of formulas f1 f2, , fm, 1. fi may be a member of S, 2. fi may be a formula deduced by using deduction rulers and formulas before it. 3. fm is .We say that we can deduce from S, denoted by S 超级计算学院 数理逻辑 第 0 章 introduction Example prove: Proof (1)p s P (2)p T(1)I (3)s T(1)I (4)p (q r

14、) P (5)q r T(2)(4)I (6)s q P (7)q T(3)(6)I (8)r T(5)(7)I,),(spqsrqp r 超级计算学院 数理逻辑 第 0 章 introduction Attached rulers (附加规则) For following reasoning prove CAHHHn,.,21.,.,21CAHHHn.).()().()().(21212121CAHHHCAHHHCAHHHCAHHHnnnn 超级计算学院 数理逻辑 第 0 章 introduction Example : prove using attached promise: Proof

15、 (1)p (q r) P (2)p P(attachment) (3)q r T(1)(2)I (4)q p P (5)q p T(4)E (6)q T(2)(5)I (7)r T(3)(6)I (8) s r P.,),(sprspqrqprs)9(s)10( 超级计算学院 数理逻辑 第 0 章 introductionCounter proof(反证法)If we want to proveWe negate C, get C, add the negation to the premise set, then deduce a contradiction,such as S S.CHH

16、Hn,.,21CHHHn,.,21CHHHn.21永真CHHHn).(21永假).(21CHHHn永假CHHHn.21Is validIs falseIs validIs false 超级计算学院 数理逻辑 第 0 章 introduction Example : using counter proof Prove (1)(p) P(attachment) (2)p T(1)E (3)r q P (4)q T(3)I (5)p q T(2)(4)I (6)p qr P (7)r T(5)(6)I (8)r T(3)I (9)r r T(7)(8)I.,pqrrqp 超级计算学院 数理逻辑 第

17、0 章 introductionIt need to notice that the deduction is carried out on the symbols, it is not relevant with semantics 超级计算学院 数理逻辑 第 0 章 introduction1.4.3 Soundness of propositional logic Definition Definition (suitable assignment, model, satisfiable, valid)Let F be a formula and let A be an assignme

18、nt, i.e. a mapping from a subset of A1,A2,. to 0, 1. If A is defined for every atomic formulaAi occurring in F, then A is called suitable for F(interpretation). 超级计算学院 数理逻辑 第 0 章 introductionIf A is suitable for F, and if A(F) = 1, then we write A F. In this casewe say F holds under the assignment ,

19、 or A is a model for F. Otherwise we write A F, and say: under the assignment A, F does not hold, or A is not a model for F 超级计算学院 数理逻辑 第 0 章 introductionA formula F is satisfiable if F has at least one model, otherwise F is called unsatisfiable or contradictory. Similarly, a set M of formulas is sa

20、tisfiableif there exists an assignment which is a model for every formula F in M.(Note that this implies that this assignment is suitable for every formula in M).A formula F is called valid (or a tautology) if every suitable assignment for F is a model for F. 超级计算学院 数理逻辑 第 0 章 introductionDefinition

21、 1.34 (semantic entailment) If for all evaluation in which all 1, 2, , n evaluate to T, evaluate to T as well, we say that 1, 2, , n Holds and call the semantic entailment relation. 超级计算学院 数理逻辑 第 0 章 introductionTheorem 1.35 (Soundness)Let 1, 2, , n and be propositional logic formulas.If 1, 2, , n i

22、s valid, then 1, 2, , n 超级计算学院 数理逻辑 第 0 章 introductionProve p q r p (q r)( page 47)Proof 1. p (attachment) 2. q (attachment) 3. p q from 1,2 4. p q r P 5. r from 3, 4 6. q r from 2, 5 7. p (q r) from 1, 6 超级计算学院 数理逻辑 第 0 章 introduction1.4. 4 Completeness of propositional logicIf 1, 2, , n , then we

23、can use deduction to get 1, 2, , n , 超级计算学院 数理逻辑 第 0 章 introduction1.5 Normal Forms1.5.1 Semantic equivalence, satisfiability and validityDefinition (semantic equivalence) Let and be formulas of propositional logic, we that and are semantic equivalence, iff and , In that case we write , Furthermore,

24、 We call valid if holds. 超级计算学院 数理逻辑 第 0 章 introductionDefinition (Conjunctive Normal Form, CNF) A literal L is either an atom form p or the negation of an atom p, A formula C is a conjunctive normal form(CNF) If it is a conjunction of clauses, where each clause D is a disjunction of literals L:= p|

25、 p D:= L| L D C:= D| D CExample: ( q p r ) ( p r) q(p r ) ( p r ) (p r)(q r r) ( q p) 超级计算学院 数理逻辑 第 0 章 introductionLemma A disjunction of literals L1 L2 , , Lm, is valid iff there are 1i,j m such Li is Lj. Definition (satisfiable) Given a formula in propositional logic, we say that is satisfiable i

26、f there has an interpretation I shch that I .Proposition 1.45 Let be a formula of propositional logic, then is satisfiable iff is not valid. 超级计算学院 数理逻辑 第 0 章 introduction1.5.2 Conjunctive Normal Form and Validity The steps of Transforming a formula into a equivalent CNF1. Remove the implication sym

27、bols by using p q= p q procedure IMPLY_FREE2. Move the negation symbols inside to the front of atoms by using Morgan Law (p q)= p q (p q)= p q procedure NNF 超级计算学院 数理逻辑 第 0 章 introduction1.5.3 Horn clauses and satisfiability The main ideas and steps of Transforming a formula into a equivalent CNF1.

28、Remove the implication symbols by using p q= p q procedure IMPLY_FREE 超级计算学院 数理逻辑 第 0 章 introduction2. Move the negation symbols inside to the front of atoms by using Morgan Law (p q)= p q (p q)= p q procedure NNF3. Transform into the desired CNF by using Distribution Law p (q r)=( p q) ( p r) (q r)

29、 p =( q p) ( r p) procedure DISTR 超级计算学院 数理逻辑 第 0 章 introductionHow to transform a formula into CNF in procedureFunction CNF(?): ? is implication free and in NNF the output of CNF(?) is an equivalent CNF. begin case ? is a literal; return ? ? is ?1 ?2; return CNF(?1) CNF(?2) ? is ?1 ?2; return CNF(?

30、1) CNF(?2) end case end 超级计算学院 数理逻辑 第 0 章 introduction 超级计算学院 数理逻辑 第 0 章 introduction1. Example ( p q)(p (r q) = ( p q) (p ( r q) = ( p q) (p ( r q) = ( p q p) ( p q r q) = ( p q ) 超级计算学院 数理逻辑 第 0 章 introduction1.5.3 Horn clauses and satisfiabilityDefinition (Horn formula) A Horn formula is formula

31、of propositional logic if it can be generated as an instance of H in this grammar: P:= | T | p A:= P| P A C:= AP H:= C | C HWe call each instance of C a Horn clause. 超级计算学院 数理逻辑 第 0 章 introductionExample: (p q s p ) (p r p ) (p s s ) (p q s ) (p r p ) (T s ) (p2 p3 p5 p13 ) ( T p5 ) (p5 p11 )No Horn

32、 formula(p q s p ) (p r p ) (p s s )(p q s s ) ( p r p ) (T s ) 超级计算学院 数理逻辑 第 0 章 introductionAlgorithm to decide the satisfiability of Horn formula1. It mark T if it occurs in that list.2. If there is a conjunct P1 P2 Pki P such that all Pj with 1j ki are marked, mark P as well and go to 2. Otherwi

33、se go to 3.3. If is marked, print out “The Horn formula is unsatisifiable” and stop, Otherwise go to 4.4. print out “The Horn formula is satisfiable” and stop. 超级计算学院 数理逻辑 第 0 章 introductionRunning the above algorithm (p q)(p q r ) (T p ) (p s u )Satisfiable (p q)(p q s ) (T p ) (p s )Unsatisfiable

34、超级计算学院 数理逻辑 第 0 章 introduction1.6 SAT solver For any formula, if the formula is satisfiable, give an interpretation, under which the formula is true. Many practical problems can be transformed into solving a SAT problem Planning and SAT problems. 超级计算学院 数理逻辑 第 0 章 introduction 例从p, q, r, s四人中选派2人出差,

35、求满足下列3个条件的选派方法有哪几种. (1)若p去,则r和s中只去1人； (2)q和r不能都去； (3)若r去, 则s不能去. Solution p: p去出差, q: q去出差, r: r去出差, s: s去出差,则 (1) (2) (3);(srp);(rq. sr 超级计算学院 数理逻辑 第 0 章 introduction (a)p, s去; (b)q, s去; (c)p, r去.?1)()()()()()()()(srqsrpsqpsrrpsrrqsrpA 超级计算学院 数理逻辑 第 0 章 introduction1.6.1 A Linear solver := p| ( )|

36、Translate the formula into a directed acyclic grapy: T()=p, T( )= T(), T(1 2)= T(1) T ( 2) T(1 2)= ( T (1) T( 2) T(1 2)= (T(1) T( 2) 超级计算学院 数理逻辑 第 0 章 introductionExample p (q p)Transform it intop ( q p) 超级计算学院 数理逻辑 第 0 章 introductionpqTFTT 超级计算学院 数理逻辑 第 0 章 introductionExample: Prove:(p q r) ( p (q

37、 r)We prove ( (p q r) ( p (q r) is unsatisfiable. 超级计算学院 数理逻辑 第 0 章 introductionIts conjunction parent and frr force FIts children and ti force TpqT :( (p q) r) ( p (q r)FTT : p (q r) “4”=“3” ”2”rTF : (p q) r)“2”=(p ( q r)“3”=(p q) r) 超级计算学院 数理逻辑 第 0 章 introduction1.6.1 A Cubic solver(p (q r) (p q )

38、 (q r) (r p ) ( p ( q r) (1.11)(1.11) is unsatisfiable. 超级计算学院 数理逻辑 第 0 章 introductionpqFTT :( r p) rT ( p ( q r)( q r)(p (q r) (p q )TTFFFF 超级计算学院 数理逻辑 第 0 章 introductionpqFTT :( r p) rT ( p ( q r)( q r)(p (q r) (p q )TTFe:FFaTFcTcTgFTbFContradiction 超级计算学院 数理逻辑 第 0 章 introductionSAT problem is dif

39、ficult, there is not common methods.We must deal with SAT problem shrewdly.You may try the following methods:1. Semantic analyzing2. Negation, then use main disjunction normal form3. Resolution 超级计算学院 数理逻辑 第 0 章 introductionS1 SupplementThe proposition resolution method1. Why we need resolution2. Pr

40、opositional resolvent3. Resolution proof4. The soundness and the completenessReference book:Logic for Computer ScientistsAuthors:Uwe Schning ISBN: 978-0-8176-4762-9 (Print) 978-0-8176-4763-6 (Online) 超级计算学院 数理逻辑 第 0 章 introductionS1.1 Why we need resolution The disadvantages of natural deduction1. T

41、here are too many deductive rulers to select2. The diversity of formulas is difficult to deal with 超级计算学院 数理逻辑 第 0 章 introductionS1.2 Propositional resolventDefinition (clause) each clause D is a disjunction of literals L:= p| p D:= L| L D denote the empty clause, contradiction.Example : p, q, p r ,

42、 p q r,Definition (resolvent)Let C1,C2 and R be clauses. Then R is called a vesolvent of C1 and C2 if there are two literals L1 and L2 in C1 and C2 respectively such that L1 = L2 (L1 and L2 is called complementary pair ) , i.e.C1= L1 D1, C2= L2 D2,then R = D1 D2 is called the resolvent of C1 and C2

43、超级计算学院 数理逻辑 第 0 章 introductionExample of resolvent p q r, p sThe resolvent : q r sp q r p sq r sParent clauses 超级计算学院 数理逻辑 第 0 章 introductionExercise : Give the entire list of resolvents which can be generated from the set of clausesA E B, A B C, A D EA E A C, E B B C, E B D EA B A D 超级计算学院 数理逻辑 第 0

44、 章 introductionS1.3 Resolution proofSuppose we want to prove 1, 2, , n We use the following steps:1. Transform 1, 2, , n into the sets of clauses respectively, and put it together, denoted it by C ,2. Transform the negation of into a the set of clause, denoted it by C 3. Set C0= C C ，C0 is called th

45、e original set of clauses. 4. Do resolution on the C0 ，and add the resolvents into set of clauses constantly, denoted by Ci .5. If the empty clause was found in set of clauses Ck, the proof is complete, and answer is true. 超级计算学院 数理逻辑 第 0 章 introductionExample, prove (P Q) , (Q R), P RC = PQ, QR, P

46、is transformed into C = RC0 = PQ, QR, P, R 超级计算学院 数理逻辑 第 0 章 introductionResolution process1. PQ, 2. QR, 3. P, 4. R,5. Q from 1, 3.6. Q from 2, 4.7. from 5, 6. 超级计算学院 数理逻辑 第 0 章 introduction PQ Q Q R QRPResolution refutation tree 超级计算学院 数理逻辑 第 0 章 introductionP (QR)，(SR)， P, S QResolution ProofThe s

47、et of clauses coming from the set of premises P QR， S R， P, S The set of clauses coming from the conclusion Q 超级计算学院 数理逻辑 第 0 章 introductionPut the above sets of clauses together, we get the original set of clauses =1. P QR， 2. S R，3. P, 4. S , 5. Q 6. P R from 1, 57. R from 2, 48. P from 6, 79. fro

48、m 3, 8 超级计算学院 数理逻辑 第 0 章 introduction P QR P R R S S R Q P P Resolution refutation tree 超级计算学院 数理逻辑 第 0 章 introductionS1.4 The soundness and completenessResolution LemmaLet F be a CNF formula, represented as set of clauses. Let R be a resolvent of two clauses C1 and C2 in F. Then, F and F U R are eq

49、uivalent.Resolution Theorem (of propositional logic)A clause set F is unsatisfiable if and only if can be obtained by adding resolvents. 超级计算学院 数理逻辑 第 0 章 introduction数理逻辑练习数理逻辑练习1 1姓名姓名 学号学号 1.1.什么是可满足的命题逻辑公式？什么是恒真的命什么是可满足的命题逻辑公式？什么是恒真的命 题逻辑公式？分别举例说明题逻辑公式？分别举例说明. .2.2.什么是命题逻辑的解释？举例说明什么是命题逻辑的解释？举例说明

50、. . 3.3.设设P,Q,R,SP,Q,R,S是任意命题公式，是任意命题公式， 判断下列公式的类型判断下列公式的类型. . (1) (R (1) (R (P (P R) R) ( (Q (Q P P) ) P P) ). . (2) (2) （P PR R） (Q (Q S) S) (P P Q Q）R)R). . 4.4. 证明证明 Q Q (P(PR)R)， (U(U V) P, Q V) P, Q (U (U V V) )R R 超级计算学院 数理逻辑 第 0 章 introduction数理逻辑练习数理逻辑练习2 2姓名姓名 学号学号 1. 1. 利用归结方法证明利用归结方法证明(p