Master of Science in Artificial Intelligence, 2009-2011 Knowledge Representation and Reasoning University "Politehnica" of Bucharest Department of Computer Science Fall 2009 Adina Magda Florea http://turing.cs.pub.ro/krr_09 curs.cs.pub.ro Lecture 4 Modal Logic Lecture outline Introduction Modal logic in CS Syntax of modal logic Semantics of modal logic Logics of knowledge and belief Temporal logics 2 1. Introduction In first order logic a formula is either true or false in any model In natural language, we distinguish between various “modes of truth”, e.g, “known to be true”, “believed to be true”, “necessarily true”, “true in the future” • “Barack Obama is the president of the US” is currently • true but it will not be true at some point in the future. “After program P is executed, A hold” is possibly true if the program performs what is intended to perform. 3 History Classical logic is truth-functional = truth value of a formula is determined by the truth value(s) of its subformula(e) via truth tables for ,, ¬, and →. Lewis tried to capture a non-truth-functional notion of “A Necessarily Implies B” (A → B) We can take A → B to mean “it is impossible for A to be true and B to be false” He chose a symbol, P, and wrote PA for “A is possible”; then: • • ¬PA is “A is impossible” ¬P¬A is “not-A is impossible” Then he used the symbol N to stand for ¬P and expressed • NA := ¬P¬A “A is necessary” Because → is logical implication, we can transform it like this: • A → B := N(A → B) = ¬P¬(A → B) = ¬P¬(¬A B) = ¬P(A ¬B) 4 Modal operators P - “possibly true” N - “necessarily true” Modal logics - modes of truth: Basic modal logic: - box, and - diamond The necessity / possibility - necessary, and possible Logics about knowledge - what an agent knows / believes Deontic logic - - it is obligatory that, and - it is permissible that 5 2. Modal logic in CS Temporal logic Dynamic logic Logic of knowledge and belief Model problems and complex reasoning The Lady and the Tiger Puzzle There are two rooms, A and B, with the following signs on them: A: In this room there is a lady, and in the other room there is a tiger” B: “In one of these rooms there is a lady and in one of them there is a tiger” One of the two signs is true and the other one is false. Q: Behind which door is the lady? 6 Modeling modal reasoning The King's Wise Men Puzzle The King called the three wisest men in the country. He painted a spot on each of their foreheads and told them that at least one of them has a white spot on his forehead. The first wise man said: “I do not know whether I have a white spot” The second man then says “I also do not know whether I have a white spot”. The third man says then “I know I have a white spot on my forehead”. Q: How did the third wise man reason? 7 Modeling modal reasoning Mr. S. and Mr. P Puzzle Two numbers m and n are chosen such that 2 m n 99. Mr. S is told their sum and Mr. P is told their product. Mr. P: "I don't know the numbers. " Mr. S: "I knew you didn't know. I don't know either." Mr. P: "Now I know the numbers." Mr S: "Now I know them too." Q: In view of the above dialogue, what are the numbers? 8 3. Modal logic - Syntax Atomic formulae: p ::= p0 | p1 | p2 | q …. where pi , q are atoms in PL Formulae: ::= p | ¬ | | | | | → where and are a wffs in PL Examples: p → q p → q (p1 → p2) → ((p1) → (p2)) Schema: • → • → • ( → ) → ( → ) Schema Instances: Uniformly replace the formula variables with formulae (inference) Examples: p → p is an instance of → but p → q is not 9 Deduction in modal logic Axioms The 3 axioms of PL • • • A1. ( ) A2. ( ( )) (( ) ( )) A3. ((¬) (¬)) ( ) The axiom to specify distribution of necessity • A4. ( ) ( ) Distribution of modality 10 Deduction in modal logic Inference rules Substitution (uniform) Modus Ponens , ( ) The modal rule of necessity |- ’ « for any formula , if was proved then we can infer » 11 4. Semantics of modal logic Nonlinear model The semantics of modal logic is known as the Kripke Semantics, also called the Possible World approach Directed graph (V, E) Vertices V = {v, v1, v2, …} Directed edges {(s1,t1), (s2,t2),…} from source vertex si V to the target vertex tiV for i = 1,2,… Cross product of a set V, V x V {(v,w) | vV and wV} the set of all ordered pairs (v,w), where v and w are from V. Directed graph - a pair (V,E), where V = {v, v1, v2, …} and E V x V is a binary relation over V. 12 Semantics of modal logic A Kipke frame is a directed graph <W, R>, where: • W is a non-empty set of worlds (points, vertices) and • R W x W is a binary relation over W, called the accessibility relation. An interpretation of a wff in modal logic on a Kripke frame <W, R> is a function I : W x L → {t,f} which tells the truth value of every atomic formula from the language L at every point (in every word) in W. A Kripke model M of a formula (an interpretation which makes the formula true) is • the triple <W, R, I>, where I is an interpretation of the formula on a Kripke frame <W,R> which makes the formula true. This is denoted by M |=W 13 Semantics of modal logic Using the model, we can define the semantics of formulae in modal logic and can compute the truth value of formulae. M |=W iff M |=/W (or M |=W ¬) M |=W iff M |=W iff M |=W or M |=W M |=W → iff M |=W ¬ or M |=W M |=W and M |=W (¬ is true in W) M |=W iff w': R(w,w') M |=W' M |=W iff w': R(w,w') M |=W' 14 Examples p – I am rich q – I am president of Romania r – I am holding a PhD in CS W1 I(W1,p) = f I(W1,q) = f I(W1,r) = a W0 I(W0,p) = f I(W0,q) = f I(W0,r) = f I(W0, p) = ? I(W0, p) = ? I(W0, r) = ? I(W0, r) = ? W2 I(W2,p) = f I(W2,q) = f I(W2,r) = f 15 Examples w1 p, q, r w0 p, q, r w2 p, q, r w3 p, q, r p -Alice visits Paris q - It is spring time r - Alice is in Italy I(W0, p) = ? I(W0, p) = ? I(W0, q) = ? I(W0, q) = ? I(W0, r) = ? I(W0, r) = ? I(W1, p) = ? I(W1, p) = ? 16 Different modal logic systems The modal logic K • A1. ( ) • A2. ( ( )) (( ) ( )) • A3. ((¬) (¬)) ( ) • A4. ( ) ( ) XX “it is impossible for A to be true and B to be false” Here is an invalidating model: R(w0,w1), I(w0,p)=f, I(w1,p)=t M |=W iff w': R(w,w') M |=W' 17 Different modal logic systems The modal logic D Add axiom X X In fact, D-models are K-models that meet an additional restriction: the accessibility relation must be serial. A relation R on W is serial iff • (wW: (w'W: (w,w')R)) 18 Different modal logic systems The modal logic T Add axiom XX A T-model is a K-model whose accessibility relation is reflexive. A relation R on W is reflexive iff • (wW: (w,w)R). 19 Different modal logic systems The modal logic S4 Add axiom X X An S4-model is a K-model whose accessibility relation is reflexive and transitive. A relation R on W is transitive iff • (w1,w2,w3 wW: (w1,w2)R (w2, w3)R (w1,w3)R). 20 Different modal logic systems The modal logic B Add axiom X X A B-model is a K-model whose accessibility relation is reflexive and symmetric. A relation R on W is symmetric iff • (w1,w2W: (w1,w2)R (w2,w1)R) 21 Different modal logic systems The modal logic S5 Add the axiom X X An S5-model is a K-model whose accessibility relation is reflexive, symmetric, and transitive. That is, it is an equivalence relation Exercise: Find an S5-model in which X is false. X S5 is the system obtained if every possible world is possible relative to every 22 other world Different modal logic systems The modal logic S5 X X A relation is euclidian iff (w1,w2,w3W: (w1,w2)R (w1, w3)R (w2,w3)R) 23 Different modal logic systems D=K+D T=K+T S4 = T + 4 B=T+B S5 = S4 + B S5 symmetric transitive S4 B transitive reflexive symmetric T D reflexive serial K 24 5. Logics of knowledge and belief Used to model "modes of truth" of cognitive agents Distributed modalities Cognitive agents characterise an intelligent agent using symbolic representations and mentalistic notions: • knowledge - John knows humans are mortal • beliefs - John took his umbrella because he believed it was going to rain • desires, goals - John wants to possess a PhD • intentions - John intends to work hard in order to have a PhD • commitments - John will not stop working until getting his PhD 25 Logics of knowledge and belief How to represent knowledge and beliefs of agents? FOPL augmented with two modal operators K and B K(a,) - a knows B(a,) - a believes with LFOPL, aA, set of agents Associate with each agent a set of possible worlds Kripke model Ma of agent a for a formula Ma =<W, R, I> with R A x W X W and I - interpretation of the formula on a Kripke frame <W,R> which makes the formula true for agent a 26 Logics of knowledge and belief An agent knows a propositions in a given world if the proposition holds in all worlds accessible to the agent from the given world Ma |=W K iff w': R(w,w') Ma |=W' An agent believes a propositions in a given world if the proposition holds in all worlds accessible to the agent from the given world Ma |=W B iff w': R(w,w') Ma |=W' The difference between B and K is given by their properties 27 Properties of knowledge (A1) Distribution axiom: K(a, ) K(a, ) K(a, ) "The agent ought to be able to reason with its knowledge" ( ) ( ) (Axiom of distribution of modality) K(a, ) ( K(a,) K(a,) ) (A2) Knowledge axiom: K(a, ) "The agent can not know something that is false" (T) - satisfied if R is reflexive K(a, ) 28 Properties of knowledge (A3) Positive introspection axiom K(a, ) K(a, K(a, )) X X (S4) - satisfied if R is transitive K(a, ) K(a, K(a, )) (A4) Negative introspection axiom K(a, ) K(a, K(a, )) X X (S5) - satisfied if R is euclidian 29 Inference rules for knowledge (R1) Epistemic necessitation |- K(a, ) modal rule of necessity |- (R2) Logical omniscience and K(a, ) K(a, ) problematic 30 Properties of belief Distribution axiom: B(a, ) B(a, ) B(a, ) YES Knowledge axiom: B(a, ) NO Positive introspection axiom B(a, ) B(a, B(a, )) YES Negative introspection axiom B(a, ) B(a, B(a, )) problematic 31 Inference rules for belief (R1) Epistemic necessitation |- B(a, ) problematic modal rule of necessity |- (R2) Logical omniscience and B(a, ) B(a, ) usually NO 32 Some more axioms for beliefs Knowing what you believe B(a, ) K(a, B(a, )) Believing what you know K(a, ) B(a, ) Have confidence in the belief of another agent B(a1, B(a2,)) B(a1, ) 33 Two-wise men problem - Genesereth, Nilsson (1) A and B know that each can see the other's forehead. Thus, for example: (1a) If A does not have a white spot, B will know that A does not have a white spot (1b) A knows (1a) (2) A and B each know that at least one of them have a white spot, and they each know that the other knows that. In particular (2a) A knows that B knows that either A or B has a white spot (3) B says that he does not know whether he has a white spot, and A thereby knows that B does not know 1. KA(WA KB( WA) 2. KA(KB(WA WB)) 3. KA(KB(WB)) (1b) (2a) (3) 4. WA KB(WA) 5. KB(WA WB) 1, A2 2, A2 A2: K(a, ) 6. KB(WA) KB(WB) 7. WA KB(WB) 5, A1 4, 6 A1: K(a, ) (K(a,) K(a,)) 8. KB(WB) WA 9. KA(WA) contrapositive of 7 3, 8, R2 Proof R2: and K(a, ) infer K(a, ) 34 6. Temporal logic The time may be linear or branching; the branching can be in the past, in the future of both Time is viewed as a set of moments with a strict partial order, <, which denotes temporal precedence. Every moment is associated with a possible state of the world, identified by the propositions that hold at that moment Modal operators of temporal logic (linear) p U q - p is true until q becomes true - until Xp - p is true in the next moment - next Pp - p was true in a past moment - past Fp - p will eventually be true in the future - eventually Gp - p will always be true in the future – always Fp true U p Gp F p F – one time point G – each time point 35 Branching time logic - CTL Temporal structure with a branching time future and a single past - time tree CTL – Computational Tree Logic In a branching logic of time, a path at a given moment is any maximal set of moments containing the given moment and all the moments in the future along some particular branch of < Situation - a world w at a particular time point t, wt State formulas - evaluated at a specific time point in a time tree Path formulas - evaluated over a specific path in a time tree 36 Branching time logic - CTL CTL Modal operators over both state and path formulas From Temporal logic (linear) Fp - p will sometime be true in the future - eventually Gp - p will always be true in the future - always F – one time point G – each time point Xp - p is true in the next moment - next p U q - p is true until q becomes true - until (p holds on a path s starting in the current moment t until q comes true) Modal operators over path formulas (branching) Ap - at a particular time moment, p is true in all paths emanating from that point - inevitable p Ep - at a particular time moment, p is true in some path emanating from that point - optional p A – all path E – some path 37 LB - set of moment formula LS - set of path-formula Semantics M = <W, T, <, | |, R> - every tT has associated a world wtW M |=t iff t|| is true in the set of moments for which holds M |=t pq iff M |=t p and M |=t q M |=t p iff M |=/t p M |=s,t pUq iff (t': tt' and M |=s,t' q and (t": t t" t' M |=s,t" p)) p holds on a path s starting in the current moment t until q comes true Fp true Up Gp F p M |=t A p iff (s: sSt M |=s,t p) Ep A p s is a path, St - all paths starting at the present moment M |=s,t X p iff M |=s,t+1 p) 38 s is true in each time point (G) and in all path (A) r is true in each time point (G) in some path (E) p will eventually (F) be true in some path (E) q will eventually (F) be true in all path (A) s r s r s p s q AGs EGr r s q F - eventually G - always A - inevitable E - optional EFp AFq s r - Alice is in Italy s – Paris is the capital of France s q p -Alice visits Paris q - It is spring time 39 Each situation has associated a set of accessible words - the worlds the agent believes to be possible. Each such world is a time tree. Within these worlds, the branching future represents the choices (options) available to the agent in selecting which action to perform Similar to a decision tree in a game of chance Decision nodes Player 1 • Each arc emanating from a chance node corresponds to a possible world Dice Player 2 1/36 1/18 Chance nodes Dice Player 1 1/36 1/18 • Each arc emanating from a decision node corresponds to a choice available in a possible world 40

1/--страниц