Transcript PPT

Logics for Data and Knowledge
Representation
Modal Logic
Originally by Alessandro Agostini and Fausto Giunchiglia
Modified by Fausto Giunchiglia, Rui Zhang and Vincenzo Maltese
Outline






2
Introduction
Syntax
Semantics
Satisfiability and Validity
Kinds of frames
Correspondence with FOL
Introduction

We want to model situations like this one:
1. “Fausto is always happy” circumstances”
2. “Fausto is happy under certain

In PL/ClassL we could have: HappyFausto

In modal logic we have:
1. □ HappyFausto
2. ◊ HappyFausto
As we will see, this is captured through the notion of “possible words” and
of “accessibility relation”
3
Syntax

We extend PL with two logical modal operators:
□ (box) and ◊ (diamond)
□P : “Box P” or “necessarily P” or “P is necessary true”
◊P : “Diamond P” or “possibly P” or “P is possible”
Note that we define □P = ◊P, i.e. □ is a primitive symbol

The grammar is extended as follows:
<Atomic Formula> ::= A | B | ... | P | Q | ... | ⊥ | ⊤ |
<wff> ::= <Atomic Formula> | ¬<wff> | <wff>∧ <wff> | <wff>∨ <wff> |
<wff>  <wff> | <wff>  <wff> | □ <wff> | ◊ <wff>
4
Different interpretations
Philosophy
□P : “P is necessary”
◊P : “P is possible”
Epistemic
□aP : “Agent a believes P ” or “Agent a knows P”
Temporal logics
□P : “P is always true”
◊P : “P is sometimes true”
Dynamic logics or
logics of programs
□aP : “P holds after the program a is executed”
Description logics
□HASCHILDMALE  ∀HASCHILD.MALE
◊HASCHILDMALE  ∃HASCHILD.MALE
5
Semantics: Kripke Model

A Kripke Model is a triple M = <W, R, I> where:
 W is a non empty set of worlds
 R ⊆ W x W is a binary relation called the accessibility relation
 I is an interpretation function I: L  pow(W) such that to each
proposition P we associate a set of possible worlds I(P) in which P holds

Each w ∈ W is said to be a world, point, state, event, situation, class …
according to the problem we model

For "world" we mean a PL model. Focusing on this definition, we can see a
Kripke Model as a set of different PL models related by an "evolutionary"
relation R; in such a way we are able to represent formally - for example the evolution of a model in time.

In a Kripke model, <W, R> is called frame and is a relational structure.
6
Semantics: Kripke Model

Consider the following situation:
BeingHappy
BeingSad
1
2
3
BeingNormal
4

BeingNormal
M = <W, R, I>
W = {1, 2, 3, 4}
R = {<1, 2>, <1, 3>, <1, 4>, <3, 2>, <4, 2>}
I(BeingHappy) = {2}
7
I(BeingSad) = {1}
I(BeingNormal) = {3, 4}
Truth relation (true in a world)

Given a Kripke Model M = <W, R, I>, a proposition P ∈ LML and a possible
world w ∈ W, we say that “w satisfies P in M” or that “P is satisfied by w
in M” or “P is true in M via w”, in symbols:
M, w ⊨ P in the following cases:
1. P atomic
w ∈ I(P)
2. P = Q
M, w ⊭ Q
3. P = Q  T M, w ⊨ Q and M, w ⊨ T
4. P = Q  T M, w ⊨ Q or M, w ⊨ T
5. P = Q  TM, w ⊭ Q or M, w ⊨ T
6. P = □Q
for every w’∈W such that wRw’ then M, w’ ⊨ Q
7. P = ◊Q
for some w’∈W such that wRw’ then M, w’ ⊨ Q
NOTE: wRw’ can be read as “w’ is accessible from w via R”
8
Semantics: Kripke Model

Consider the following situation:
BeingHappy
BeingSad
1
2
3
BeingNormal
4

BeingNormal
M = <W, R, I>
W = {1, 2, 3, 4}
R = {<1, 2>, <1, 3>, <1, 4>, <3, 2>, <4, 2>}
I(BeingHappy) = {2}
9
I(BeingSad) = {1}
M, 2 ⊨ BeingHappy
M, 2 ⊨ BeingSad
M, 4 ⊨ □BeingHappy
M, 1 ⊨ ◊BeingHappy
I(BeingNeutral) = {3, 4}
M, 1 ⊨ ◊BeingSad
Satisfiability and Validity

Satisfiability
A proposition P ∈ LML is satisfiable in a Kripke model M = <W, R, I> if M, w
⊨ P for all worlds w ∈ W.
We can then write M ⊨ P

Validity
A proposition P ∈ LML is valid if P is satisfiable for all models M (and by
varying the frame <W, R>).
We can write ⊨ P
10
Satisfiability

Consider the following situation:
BeingSad
BeingHappy
1
2
3
BeingNormal
4

BeingNormal
M = <W, R, I>
W = {1, 2, 3, 4}
R = {<1, 2>, <2, 2>, <3, 2>, <4, 2>}
I(BeingHappy) = {2}
I(BeingSad) = {1}
I(BeingNormal) = {3, 4}
M, w ⊨ □BeingHappy for all w ∈ W, therefore □BeingHappy is satisfiable in
M.
11
Validity

Prove that P: □A  ◊A is valid
A
1
2
3
A

In all models M = <W, R, I>,
(1) □A means that for every w∈W such that wRw’ then M, w’ ⊨ A
(2) ◊A means that for some w∈W such that wRw’ then M, w’ ⊨ A
It is clear that if (1) then (2) in the example
(as we will see this is valid in serial frames)
12
Kinds of frames

Given the frame F = <W, R>, the relation R is said to be:






Serial
iff for every w ∈ W, there exists w’ ∈ W s.t. wRw’
Reflexive
iff for every w ∈ W, wRw
Symmetric
iff for every w, w’ ∈ W, if wRw’ then w’Rw
Transitiveiff for every w, w’, w’’ ∈ W, if wRw’ and w’Rw’’
then wRw’’
Euclidian iff for every w, w’, w’’ ∈ W, if wRw’ and wRw’’
then w’Rw’’
We call a frame <W, R> serial, reflexive, symmetric or transitive
according to the properties of the relation R
13
Kinds of frames

Serial: for every w ∈ W, there exists w’ ∈ W s.t. wRw’
1

3
Reflexive: for every w ∈ W, wRw
1

2
2
Symmetric: for every w, w’ ∈ W, if wRw’ then w’Rw
1
14
2
3
Kinds of frames

Transitive: for every w, w’, w’’ ∈ W, if wRw’ and w’Rw’’ then wRw’’
1

2
3
Euclidian: for every w, w’, w’’ ∈ W, if wRw’ and wRw’’ then w’Rw’’
1
2
3
15
Valid schemas

A schema is a formula where I can change the variables

THEOREM. The following schemas are valid in the class of indicated frames:
D:
T:
B:
4:
5:
□A  ◊A
valid for serial frames
□A  A
valid for reflexive frames
A  □◊A
valid for symmetric frames
□A  □□A
valid for transitive frames
◊A  □◊A
valid for Euclidian frames
NOTE: if we apply T, B and 4 we have an equivalence relation

THEOREM. The following schema is valid:
K:
16
□(A  B)  (□A  □B)
Distributivity of □ w.r.t. 
Proof for T: □ A  A valid for reflexive frames
Assuming M, w ⊨ □A, we want to prove that M, w ⊨ A.
From the assumption M, w ⊨ □A, we have that for every w’∈W such that
wRw’ we have that M, w’ ⊨ A (1).
Since R is reflexive we also have w’Rw, we then imply that M, w ⊨ A (by
substituting w to w’ in (1))
□A, A
1
17
2
Proof for B: A  □◊A valid for symmetric frames
Assume M, w ⊨ A. To prove that M, w ⊨ □◊A we need to show that for
every w’ ∈ W such that wRw’ then M, w ⊨ ◊A.
M, w ⊨ ◊A is that for some w’’∈W such that w’Rw’’ then M, w’’ ⊨ A.
Therefore we need to prove that for every w’∈W such that wRw’ and for
some w’’∈W such that w’Rw’’ then M, w’’ ⊨ A
Since R is symmetric, from wRw’ it follows that w’Rw. For w’’∈W such that
w’’ = w, we have that w’Rw’’ and M, w’’ ⊨ A.
Hence M, w ⊨ A.
18
A, □◊A
◊A
1
2
3
Reasoning services: EVAL

Model Checking (EVAL)
Given a (finite) model M = <W, R, I> and a proposition P ∈ LML we want to
check whether M, w ⊨ P for all w ∈ W
M, w ⊨ P for all w ?
Yes
M, P
19
EVAL
No
Reasoning services: SAT

Satisfiability (SAT)
Given a proposition P ∈ LML we want to check whether there exists a
(finite) model M = <W, R, I> such that M, w ⊨ P for all w ∈ W
Find M such that M, w ⊨ P for all w
M
P
20
SAT
No
Reasoning services: UNSAT

Unsatisfiability (unSAT)
Given a (finite) model M = <W, R, I> and a proposition P ∈ LML we want to
check that does not exist any world w such that M, w ⊨ P
Verify that ∃ w such that M, w ⊨ P
M, P
21
w
VAL
No
Reasoning services: VAL

Validity (VAL)
Given a a proposition P ∈ LML we want to check that M, w ⊨ P for all
(finite) models M = <W, R, I> and w ∈ W
Verify that M, w ⊨ P for all M and w
Yes
P
22
VAL
No
Correspondence between □ and ∀ (◊ and ∃)

We can define a translation function T: LML  LFO as follows:
1. T(P) = P(x) for all propositions P in LML
2. T(P) = T(P) for all propositions P
3. T(P * Q) = T(P) * T(Q) for all propositions P, Q and *∈{,,}
4. T(□P) = ∀x T(P) for all propositions P
5. T(◊P) = ∃x T(P) for all propositions P
THEOREM:
For all propositions P in LML, P is modally valid iff T(P) is valid in FOL.
23