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 Substitutivity of Equivalence Let A,M and N be w s and let A M N be the result of replacing M by N at zero or more occurrences (henceforth called designate occurrences) of M in A. 1. A M N is a w . 2. If j= M N then j= A A M N . ( sub) If ‘ M N then ‘ A A M N Logic in Computer Science { p.3/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 w to be a truth function? Logic in Computer Science { p.4/19 Abstraction If p 1 ; ;p n are distinct propositional variables including all variables in A, let [ p 1 p n ]A : fT; Fg n ! fT; Fg where [ p 1 p n ]A(x 1 ; ;x n ) = (A) and (p i ) = x i for all 0 i n. Obviously, [ p 1 p n ]A = [ p 1 p n ]B i A B Logic in Computer Science { p.5/19 Normal Form A literal is a w of the form p or of the form p A w is in disjunctive normal form i it is a disjunction of conjunctions of literals. m _ i=1 n i ^ j=1 p ij A w is in conjunctive normal form i it is a conjunction of disjunctions of literals. m ^ i=1 n i _ j=1 p ij Logic in Computer Science { p.6/19 Disjunctive Normal Form Theorem 1. Let h be any truth function with n arguments, where n 1, and let p 1 ; ;p n be distinct propositional variables. Then there is a w A in disjunctive normal form such that h = [ p 1 p n ]A. 2. For every w B of propositional calculus there is a w A in disjunctive normal form such that B is equivalent A. Logic in Computer Science { p.7/19 Completeness of Propositional Connectives A set of propositional connectives is complete i for each integer n 1 and for each truth function h of n arguments, there is a w A in which only connectives of occur such that h = [ p 1 p n ]A f ;_g is complete. Logic in Computer Science { p.8/19 Negation Normal Form A w of propositional calculus is in negation normal form i 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 w A in negation normal form, de ne a set C(A) of conjuncts of A by induction as follows If A is a literal, C(A) = fAg If A has the form B _ C, C(A) = C(B) [C(C) If A has the form B ^ C, C(A) = fD ^ EjD 2 C(B) and E 2 C(C)g Logic in Computer Science { p.10/19 Checking Satis ability Let A be a w in negation normal form. Let ’ be an assignment. Then j= ’ A i ’ satis es some conjunct of A. A is contradiction i every conjunct of A contains complementary literals. Logic in Computer Science { p.11/19 Resolution Logic in Computer Science { p.12/19 Clause A clause is a set of nite literals. Let l be a literal, l c is its complement. This means that if l = p then l c = p and if l = p then l = p. Logic in Computer Science { p.13/19 Resolvent Let C 1 and C 2 be clauses. If l 2 C 1 and l c 2 C 2 , then (C 1 l) [ (C 2 l c ) is resolvent of C 1 and C 2 . If C be resolvent of C 1 and C 2 , then C 1 ;C 2 ‘ C. Logic in Computer Science { p.14/19 Deduction by Resolution Let S be a set of clauses, and let C be a clause. A deduction by resolution of C from S(S‘C) is a sequence C 0 ; ;C m such that 1. C m = C 2. for each i(0 i n) (a) C i 2 S or (b) C i is a resolvent of C j and C k such that j < i and k < i. A refutation of S is a deduction of [] from S. Logic in Computer Science { p.15/19 Properties of ‘ If C 2 S then S‘C If S 0 ‘C and S 0 S then S‘C If C is a resolvent of C 1 and C 2 then C 1 ;C 2 ‘C If S 0 ‘C, and S‘C for every C 2 S 0 , then S‘C If S‘C then S ‘ C Logic in Computer Science { p.16/19 Resolution Theorem is contradictory i ‘[] Logic in Computer Science { p.17/19 Summary Logic in Computer Science { p.18/19 Propositional Calculus 1. Syntax (a) Well-Formed Formula (b) Proof and Proof System (c) Independence 2. Semantics 3. Meta Theorems (a) Soundness (b) Completeness (c) Compactness 4. Checking Satis ability Logic in Computer Science { p.19/19