CST-31105

Lecture (5)
Propositional Logic
Propositions: Example

The following are propositions

 Today is Monday
 The grass is wet
 It is raining

The following are not propositions

 C++ is the best language Opinion
 When is the pretest? Interrogative
 Do your homework Imperative

Faculty of Computer Science 2

Usefulness of Logic

 Logic is more precise than natural language

 You may have cake or ice cream.

Can I have both?

 If you buy your air ticket in advance, it is

cheaper.

Are there or not cheap last-minute tickets?

Faculty of Computer Science 3

 What is Propositional Logic?

proposition = statement
Logic = the study of the logic relationships between objects
Propositions are connected by logical operators.

e.g., “the street is wet”.

“it is raining”.
if it is raining the street is wet. (connected the above)

it is raining⇒ the street is wet. (written more formally)

Faculty of Computer Science 4

Syntax

Faculty of Computer Science 5

 The formulas defined in this way are so far purely syntactic
constructions without meaning.

Faculty of Computer Science 6

 Semantics
Two truth values: t for true, f for false
e.g., A ∧ B
 A = “It is raining today” and B = “It is cold today” (A ∧ B is true)
 B = “It is hot today” (A ∧ B is false)

 every propositional logic formula with n different variables has 2n different

interpretations.
 priorities are ordered as parentheses, Science ⇔.
(),￢,∧,∨,⇒,
Faculty of Computer 7
 Propositional Logic: Syntax and Semantics LP & AI

Precedence of Operators
Operator Precedence
() 1
¬ 2
∧ 3
Ⅴ 4
⇒ 5
⇔ 6

E.g ¬p Λq = (¬p ) Λq
p Λq Ⅴ r = (p Λq ) Ⅴ r
10
ㅡ p Ⅴ q Λr = p Ⅴ (q Λr)
17
Faculty of Computer Science 9
Faculty of Computer Science 10
 Propositional Logic: Syntax and Semantics

Explanation with example

Implication conditional statement

E.g., “Maria will find a good job when she learns discrete mathematics.”
“If Maria learns discrete mathematics, then she will find a good
job.”
 Propositional Logic: Syntax and Semantics

Explanation with example

LP & AI
Tautology A proposition which is true under all
circumstances

E.g., ‘4’ divided by ‘2’ is ‘2’.

A proposition which is false under all

Contradiction
circumstances

E.g., Kyoto is the capital of India.

Proof

Exercise 2.2, 2.4

Faculty of Computer Science 13

 Exercise
Exercise:

Which of the following implications is true?

LP & AI
 If -1 is a positive number, then 2+2=5 True
The premise is obviously false, thus no matter what
the conclusion is, the implication holds.

 If -1 is a positive number, then 2+2=4 True

Same as above
x can be a multiple of . If we let x=2, then sin x=0
but x0.
 IfThe
sinimplication
x = 0, then“if xsin= x0= 0,
False
then x = k, for some k”

x can be a multiple of . If we let x=2, then sin x=0

but x0.
17 The implication “if sin x = 0, then x = k, for some k”
ㅡ
17 is true.
 Proof Systems

 in every interpretation in which KB is true, Q is also true.

 whenever KB is true, Q is also true.
 A∨￢A is tautology, their proposition is empty.
 The empty formula is true in all interpretations. For every tautology T then ∅
| T. For short, T.

Faculty of Computer Science 15

 by the deduction theorem KB⇒Q is a tautology.
 the negation ￢(KB⇒Q) is unsatisfiable.
￢(KB⇒Q)≡￢(￢KB ∨ Q) ≡ KB∧￢Q

 Because of the equivalence A ∧ ￢A ⇔ f from Theorem 2.1, we know that a

16
contradiction is unsatisfiable. Faculty of Computer Science
 The computation time grows exponentially with the number of variables.
Therefore this process is unusable for large variable counts, at least in the
worst case.
 syntactic manipulation of the formulas KB and Q -- to avoid having to test
all interpretations with the truth table method
 by application of inference rules with the goal of greatly simplifying them
 call this syntactic process derivation and write KB Q
 Such syntactic proof systems are called calculi.

Faculty of Computer Science 17

 Soundness – Every formula that can be proved in the system is
logically valid with respect to the semantics of the system.
 The soundness of a calculus ensures that all derived formulas are in
fact semantic consequences of the knowledge base.

 A complete calculus always finds a proof if the formula to be

proved follows from the knowledge base.

Faculty of Computer Science 18

Conjunctive Normal Form (CNF)
 To keep automatic proof systems as simple as possible

Faculty of Computer Science 19

Example 2.1

Exercise 2.3

Faculty of Computer Science 20

• modus ponens, a simple, intuitive rule of inference, which, from
the validity of A and A⇒B, allows the derivation of B.

• Modus ponens as a rule by itself, while sound, is not complete.

• eg., If today is Tuesday then John will go to work. (A⇒B)

Today is Tuesday. (A)
Therefore, John will go to work. (B)

Faculty of Computer Science 21

 Proof Systems and Resolution

LP & AI
Modus Ponens

Resolution rule, A ∨ B, ¬B ∨ C
A∨C

A ∨ B, B ⇒ C
(resolvent)
A∨C

If A is false then ?

12
ㅡ
18
 Resolution

 B and ￢B is called complementary.

 The resolution rule deletes a pair of complementary literals from the two
clauses and combines the rest of the literals into a new clause.

Faculty of Computer Science 23

 “Consistent”
Proof Systems and Resolution

A formula KB is called consistent if it is impossible

to derive from it a contradiction, that is, a formula of
the form φ ∧ ¬φ.

 implementation simpler
24  search space is reduced and computation time
ㅡ
17 decreased.
 Proof Systems and Resolution

Formalization

Resolution Transformation
Proof into normal form

Proof
25
ㅡ
17
• Example 2.2
• Despite studying English for seven long years with brilliant success, I
must admit that when I hear English people speaking English I'm
totally perplexed.
• Recently, moved by noble feelings, I picked up three hitchhikers, a
father, mother, and daughter, who I quickly realized were English and
only spoke English. At each of the sentences that follow I wavered
between two possible interpretations. They told me the following (the
second possible meaning is in parentheses):
• The father: We are going to Spain (we are from Newcastle). The
mother: We are not going to Spain and are from Newcastle (we
stopped in Paris and are not going to Spain). The daughter: We are not
from Newcastle (we stopped in Paris). What about this charming
English family?

Faculty of Computer Science 26

• S = “We are going to Spain”,
• N = “We are from Newcastle”, and
• P = “We stopped in Paris”

(S ∨ N) ∧ [(￢S ∧ N) ∨ (P ∧￢S)] ∧ (￢N ∨ P).

(formalization) The father: We are going to Spain (we are from
Newcastle). The mother: We are not going to
Spain and are from Newcastle (we stopped in
Paris and are not going to Spain). The daughter:
We are not from Newcastle (we stopped in
Paris). What about this charming English
family?
Faculty of Computer Science 27
• S = “We are going to Spain”,
• N = “We are from Newcastle”, and
• P = “We stopped in Paris”

• (S ∨ N) ∧ [(￢S ∧ N) ∨ (P ∧￢S)] ∧ (￢N ∨ P). (formalization)

• (S ∨ N) ∧ (￢S) ∧ (P ∨ N) ∧ (￢N ∨ P). (CNF)

• KB ≡ (S ∨ N)1 ∧ (￢S)2 ∧ (P ∨ N)3 ∧ (￢N ∨ P)4.

(1) Res(1, 2) : (N)5 (2) Res(3, 4) : (P )6 (3) Res(1, 4) : (S ∨ P)7

• (S)8 is added.

• Res(2, 8) : ()9

• ￢S ∧ N ∧ P holds.

• The “charming English family” evidently comes from Newcastle, stopped in

Paris, but is not going to Spain.
Faculty of Computer Science 28
Example 2.3
Three girls practice high jump for their physical education final exam. The bar is
set to 1.20 meters. “I bet”, says the first girl to the second, “that I will make it
over if, and only if, you don’t”. If the second girl said the same to the third, who
in turn said the same to the first, would it be possible for all three to win their
bets?

Formalization:
• The first girl’s jump succeeds: A, First girl’s bet: (A ⇔ ￢B),
• the second girl’s jump succeeds: B, second girl’s bet: (B ⇔ ￢C),
• the third girl’s jump succeeds: C. third girl’s bet: (C ⇔ ￢A).
Claim: the three cannot all win their bets:
Q≡￢((A ⇔ ￢B) ∧ (B ⇔ ￢C) ∧ (C ⇔ ￢A))
It must now be shown by resolution that ￢Q is unsatisfiable.

(A ⇔ ￢B) ≡ (A⇒￢B) ∧ (￢B ⇒A) ≡ (￢A∨￢B) ∧ (A ∨ B) (First girl’s bet: CNF)

￢Q≡ (￢A∨￢B)1 ∧ (A ∨ B)2 ∧ (￢B ∨￢C)3 ∧ (B ∨ C)4 ∧ (￢C ∨￢A)5 ∧ (C ∨ A)6.
Res(1, 6) : (C ∨￢B)7 Res(4, 7) : (C)8
Res(2, 5) : (B ∨￢C)9 Res(3, 9) : (￢C)10
Res(8, 10) : () Faculty of Computer Science 29
 Horn LP & AI

Clauses
Case Study: Answer

Formalization
• The first girl’s jump succeeds: A,
First girl’s bet: (A ⇔ ￢B),
• The second girl’s jump succeeds: B,
Second girl’s bet: (B ⇔ ￢C),
• The third girl’s jump succeeds: C.
Third girl’s bet: (C ⇔ ￢A).
30
ㅡ
17 Claim: the three cannot all win their bets:
Q≡￢((A ⇔ ￢B) ∧ (B ⇔ ￢C) ∧ (C ⇔ ￢A))
 Horn LP & AI

Clauses
Case Study: Answer

CNF

 It must now be shown by resolution that ￢Q is

unsatisfiable.

(A ⇔ ￢B) ≡(A⇒￢B) ∧ (￢B ⇒A) ≡(￢A∨￢B) ∧ (A ∨ B)

(First girl’s bet: CNF)

￢Q≡ (￢A∨￢B)1 ∧ (A ∨ B)2 ∧ (￢B ∨￢C)3 ∧ (B ∨ C)4 ∧ (￢C

∨￢A)5 ∧ (C ∨ A)6.
31
ㅡ
17
 Horn LP & AI

Clauses
Case Study: Answer

Resolution Proof

Res(1, 6) : (C ∨￢B)7
Res(4, 7) : (C)8
Res(2, 5) : (B ∨￢C)9
Res(3, 9) : (￢C)10
Res(8, 10) : ()
32
ㅡ
17
 Horn Clauses
clause in CNF  (￢A1 ∨・・・∨￢Am ∨ B1 ∨・・・∨Bn) ≡or (equivalently)

A1 ∧・・・∧Am⇒B1 ∨・・・∨Bn
e.g., “If the weather is nice and there is snow on the ground, I will go skiing
or I will work.”
 The receiver of this message knows for certain that the sender is not going
swimming.

• “If the weather is nice and there is snow on the ground, I will go skiing.”.
 The receiver now knows definitively.
• clauses with at most one positive literal is called definite clauses.
• These clauses have the advantage that they only allow one conclusion and
are thus distinctly simpler to interpret.

Faculty of Computer Science 33

 Horn LP & AI

Clauses
Horn Clauses : Definition

Clauses with at most one positive literal of the form

(¬A1 ∨ ··· ∨ ¬Am ∨ B) or (¬A1 ∨ ··· ∨ ¬Am) or B

or (equivalently)
A1 ∧ ··· ∧ Am ⇒ B or A1 ∧ ··· ∧ Am ⇒ f or B.

A clause with a single positive literal is a fact.

In clauses with negative and one positive literal,

the positive literal is called the head.
6
—
19
 Horn LP & AI

Clauses
(nice_weather)1 (snowfall⇒snow)3

(nice_weather ∧
(snowfall)2 snow⇒skiing)4

 to know whether skiing holds, let’s use generalized modus ponens as an inference rule

A1 ∧・・・∧Am, A1 ∧・・・∧Am⇒B
B
MP(2, 3) : (snow)5 MP(1, 5, 4) : (skiing)6

1 In this case, modus ponens can derive many unnecessary formulas if one begins with
the wrong clauses.
7
— 2 Modus ponens use forward chaining systems, which start with facts and finally derive
19 the query
 Horn LP & AI

Clauses
Backward Chaining

• starts with the query and works backward until the

facts are reached.

• for backward chaining of Horn Clauses, SLD

(“Selection rule driven linear resolution for definite
clauses”) resolution is used.
36
ㅡ
17
 Horn Clauses LP & AI

Forward Vs Backward Chaining

Forward Chaining Backward Chaining

 data driven inference  goal driven inference
technique technique
 starts from a new data  starts from possible conclusion
and aims for any or goal and aims for necessary
conclusion data
 bottom up reasoning  top down reasoning

ㅡ
37  breadth first search  depth first search
17
 infinite number of  Reasonable number of
possible conclusions possible final answers
 Horn LP & AI

Clauses
SLD Resolution Proof

 (nice_weather)1
 (snowfall)2
 (snowfall⇒snow)3
 (nice_weather ∧ snow⇒skiing)4
 (skiing⇒f )5

38
ㅡ
17  Res(5, 4) : (nice_weather ∧
snow⇒f )6
 Res(6, 1) : (snow⇒f )7
 Res(7, 3) : (snowfall⇒f )8
 Res(8, 2) : ()
 Horn Clauses LP & AI

SLD Resolution Proof

 “linear resolution” means that further processing

is always done on the currently derived clause.

 great reduction of the search space

 the literals of the current clause are always

processed in a fixed order (from right to left)
39
ㅡ
17
 Computability and Complexity
Truth table method
• simplest semantic proof system
• can determine every model of any formula in finite time (unsatisfiable,
satisfiable, valid formula)
• computation time grows in the worst case exponentially with the number n of
variables.
• many clauses with few variables, the truth table method is preferable
Semantic trees
• avoid looking at variables that do not occur in clauses
• save computation time, but in worst case it is exponential
Resolution
• in the worst case the number of derived clauses grows exponentially with the
number of initial clauses.
• few clauses with many variables, resolution will probably finish faster.
Horn clauses
• Computation time grows only linearly as the number of literals in the formula
increases
Faculty of Computer Science 40
 Horn LP & AI

Clauses
Applications and Limitations
• propositional logic is
employed in simple
applications

Application

• the variables must all be discrete,

• 41 simple expert systems with only a few values, and there
ㅡ E.g.
17 can certainly work with
Limitation
may not be any cross relations
propositional logic. between variables.
 Horn LP & AI

Clauses
Exercise

Let KB consists of the following

sentences:
¬(P ∧ ¬Q) ∨ ¬(¬S ∧ ¬T) ,
¬(T ∨ Q),
U ⇒ (¬T ⇒ (¬S ∧ P))
Prove that ¬U holds using resolution.
1
1 Simplify each formula
¬(P ∧ ¬Q) ∨ ¬(¬S ∧ ¬T) ≡ ¬P ∨ Q ∨ S ∨ T
¬(T ∨ Q) ≡ ¬T ∧ ¬Q
U ⇒ (¬T ⇒ (¬S ∧ P)) ≡ U ⇒ (¬(¬T) ∨ (¬S ∧ P))
≡ U ⇒ (T ∨ (¬S ∧ P))
16
ㅡ ≡ ¬U ∨ T ∨ (¬S ∧ P)
19 ≡ (¬U ∨ T ∨ ¬S) ∧ (¬U ∨ T ∨ P)
 Horn LP & AI

Clauses
Exercise

2 Transform to CNF
(¬P ∨ Q ∨ S ∨ T)1 ∧
(¬T)2 ∧ (¬Q)3 ∧

(¬U ∨ T ∨ ¬S)4 ∧ (¬U ∨ T ∨ P)5 ∧ (U)6

43
ㅡ
17
 Horn LP & AI

Clauses
Exercise

3 Resolution Proof

Res(4,1) : ¬U ∨ T ∨ ¬S,¬P ∨ Q ∨ S ∨ T
(¬U ∨ T ∨ ¬P ∨ Q)7
Res(7,5) : ¬U ∨ T ∨ ¬P ∨ Q, ¬U ∨ T ∨ P
(¬U ∨ T ∨ Q)8
Res(8,3) : ¬U ∨ T ∨ Q, ¬Q
(¬U ∨ T) 9

44 Res(9,2) : ¬U ∨ T, ¬T
ㅡ (¬U) 10
17
Res(6,10): ()
 Horn LP & AI

Clauses
Practice

1 Show that the formula is tautology.

2 Check the statements for satisfiability or validity.

3 Formalize the statement.

4 Transform the formula to CNF.

5 Proof the formula by resolution calculus.

45
ㅡ
17 6 Proof the formula by SLD resolution.
 Applications and Limitations
• In AI, propositional logic is employed in simple applications.

• For example, simple expert systems can certainly work with propositional logic.

• However, the variables must all be discrete, with only a few values, and there
may not be any cross relations between variables.

Faculty of Computer Science 46

 Exercise

• Exercise 2.2, 2.3, 2.4, 2.11, 2.13

Faculty of Computer Science 47

 Reference

• Introduction to Artificial Intelligence (Undergraduate Topics in Computer

Science) by Wolfgang Ertel, Nathanael T. Black, Springer; 2011 edition
(March 15, 2011)

Faculty of Computer Science 48