Artificial Intelligence:

Propositional Logic and Resolution

INT3401 21
Instructor: Nguyễn Văn Vinh, UET - Hanoi VNU
2020

5/4/2020
 The Big Picture

General Search:
states are arbitrary

CSPs
structured states: vars ∊ domains
constraint propagation

Satisfiability:
variables ∊ {true, false}
Constraint Manipulation: constraints = logical formulae
cycle cutset; tree
decomposition
Constraint Manipulation:
resolution theorem proving

2 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020

 Logical Reasoning as CSP

Find variable assignments (“models”) that satisfy all

constraints.

Wumpus World
Bij = breeze felt

Sij = stench smelt

Pij = pit here

Wij = wumpus here

G = gold

3 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020

 Constraint Language: Syntax

 Sentence: atomic or complex

 Atomic sentence: P, Q, R, …, True, False
 Complex sentence:
 (Sentence) | [Sentence]
 ¬ Sentence “negation”
 Sentence ∧ Sentence “conjunction”
 Sentence ∨ Sentence “disjunction”
 Sentence ⇒ Sentence “implies” / “if-then”
 Sentence ⇔ Sentence “biconditional” / “iff”

4 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020

 Notes on Connectives

𝛂 ∨ 𝛃 is inclusive or, not exclusive

𝛂 ⇒ 𝛃 is equivalent to ¬𝛂 ∨ 𝛃
 Says who?

𝛂 ⇔ 𝛃 is equivalent to (𝛂 ⇒ 𝛃) ∧ (𝛃 ⇒ 𝛂)
 Prove it!

5 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020

 𝛂 ⇒ 𝛃 is equivalent to ¬𝛂 ∨ 𝛃

𝛂 𝛃 𝛂⇒𝛃 ¬𝛂 ¬𝛂 ∨ 𝛃
F F T T T
F T T T T
T F F F F
T T T F T

When two expressions produce the same result in

all possible models, their equivalence is a
tautology.
6 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020
 𝛂 ⇔ 𝛃 is equivalent to (𝛂 ⇒ 𝛃) ∧ (𝛃 ⇒ 𝛂)

𝛂 𝛃 𝛂⇔ 𝛂 ⇒ 𝛃 𝛃 ⇒ 𝛂 (𝛂⇒𝛃) ∧ (𝛃⇒𝛂)
𝛃
F F T T T T
F T F T F F
T F F F T F
T T T T T T

The equivalence is a tautology because it’s true in all

models. Expressed as a logical sentence:
(𝛂 ⇔ 𝛃) ⇔ [(𝛂 ⇒ 𝛃) ∧ (𝛃 ⇒ 𝛂)]
7 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020
 Literals

 Positive literal: P
 Negative literal: ¬ P
 Literals represent simple claims about the world.
 Literal sentences are unary constraints on the
model.

Literal (Unary Constraint) Model

P P = True

¬P P = False

8 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020

 Sentences As Constraints

A sentence with n variables functions as an n-ary

constraint on possible models:
P Q R
[(p ∧ ¬q) ∨ (q ∧ ¬p)] ⇒ r
false false false

false false true

false true false

Possible
false true true
Models
true false false

true false true

true true false

true true true

9 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020

 Semantics: Entailment

 𝛂 ⊨ 𝛃 if and only if, in every model in which 𝛂 is

true, 𝛃 is also true.

 M(𝛂) denotes the set of all models of 𝛂.

 𝛂 ⊨ 𝛃 means M(𝛂) ⊆ M(𝛃)

10 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020

 Semantics: Grounding

11 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020

 Inference By Model Checking

𝛂1is models with no pit at

1,2.
𝛂1 = M(¬P1,2) At 1,1: nothing.
¬P1,1 , ¬B1,1
At 2,1: breeze KB
B2,1 , ¬P2,1

Constraints:
P2,1⇒ B1,1∧B2,2∧ B3,1
B2,1⇔ P1,1∨ P2,2 ∨P3,1

12 All models consistent

Nguyenwith KB–and
Van Vinh UET, VNU Hanoi 5/4/2020
constraints.
 Inference By Model Checking

𝛂2is models with no pit at

2,2
𝛂2 = M(¬P2,2) At 1,1: nothing.
¬P1,1 , ¬B1,1
At 2,1: breeze KB
B2,1 , ¬P2,1

Constraints:
P2,1⇒ B1,1∧B2,2∧ B3,1
B2,1⇔ P1,1∨ P2,2 ∨P3,1

13 All models consistent with

Nguyen VanKB
Vinhand
– UET, VNU Hanoi 5/4/2020
constraints.
Wumpus World Agent

Step Agent Action Tell KB

(variable assignment)

1 Start at 1,1. Sense: nothing. ¬ P1,1 , ¬ B1,1

Model check. Relevant constraints:

P2,1 ⇒ B11 , P1,2 ⇒ B11 ¬ P2,1 , ¬ P1,2
Constraint is false in any model with P2,1.
So KB ⊧ ¬ P2,1. Similarly, KB ⊧ ¬ P1,2.
2 Agent moves to 2,1. Sense: breeze. B2,1

Model check. Relevant constraints:

B2,1 ⊧ P1,1 ∨ P2,2 ∨ P3,1 --
There could be a pit at 2,2 or 3,1 or both.
Can’t infer any new literals.
14 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020
Wumpus World Agent

Step Agent Action Tell KB

(variable assignment)

3 Agent returns to 1,1. --

4 Agent moves to 1,2. Sense stench, no breeze. ¬ B1,2

Model check. Relevant constraints:

P2,2 ⇒ B12 , P1,3 ⇒ B12 ¬ P2,2 , ¬ P1,3
Constraint is false in any model with P2,2.
So KB ⊧ ¬ P2,2. Similarly, KB ⊧ ¬ P1,3.

Another relevant constraint:

B1,2 ⇔ (P1,1 ∨ P2,2 ∨ P3,1) P3,1
Constraint propagation gives: P3,1.

15 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020

 Cost of Model Checking Inference

 A 4x4 wumpus world has 16 squares.

 Four variables per square: Pij, Bij, Sij, Wij
 There are 64 variables.

 Search space is 264 possible models!

 This could take a while…

 What can we do?

16 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020

 Option 1: Exploit Locality

 A constraint only references a square and its

four neighbors.
 Solve subproblems for smaller regions.
 Share variable assignments across subproblems to get
a global solution.

 Constraints on P/B don’t mention S or W.

Constraints on S/W don’t mention P or B.
 Separate the P/B and S/W models.
 Reduces state space from 2n to 2×2n/2.
17 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020
 Option 2: Go Meta

 Instead of searching the space of models, let’s

search the space of constraints (logical formulae).

 Adopt inference rules to derive new formulae

from old.
 This is called theorem proving.

 Deriving new literals will directly give us valid

models.

18 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020

 Inference Rule 1: Modus Ponens

Latin for “mode that affirms”.

𝛂⇒𝛃 , 𝛂
____________________

19 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020

 Inference Rule 2: And-Elimination

𝛂∧𝛃
_______________

20 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020

 Inference Rule 3: And-Introduction

𝛂 , 𝛃
_______________

𝛂∧𝛃

21 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020

 Inference Rules Resulting From Logical Equivalences
(1/4)

 Commutativity:
(𝛂 ∧ 𝛃) ≡ (𝛃 ∧ 𝛂)
(𝛂 ∨ 𝛃) ≡ (𝛃 ∨ 𝛂)

 Associativity:
((𝛂 ∧ 𝛃) ∧ 𝛄) ≡ (𝛂 ∧ (𝛃 ∧ 𝛄))
((𝛂 ∨ 𝛃) ∨ 𝛄) ≡ (𝛂 ∨ (𝛃 ∨ 𝛄))

22 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020

 Inference Rules Resulting From Logical Equivalences
(2/4)

 Double-negation elimination:
¬(¬𝛂) ≡ 𝛂

 Contraposition:
(𝛂 ⇒ 𝛃) ≡ (¬𝛃 ⇒ ¬𝛂)

23 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020

 Inference Rules Resulting From Logical Equivalences
(3/4)

 Implication elimination:
(𝛂 ⇒ 𝛃) ≡ (¬𝛂 ∨ 𝛃)

 Biconditional elimination:
(𝛂 ⇔ 𝛃) ≡ ((𝛂 ⇒ 𝛃) ∧ (𝛃 ⇒ 𝛂))

24 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020

 Inference Rules Resulting From Logical Equivalences
(4/4)

 De Morgan’s Laws:
¬ (𝛂 ∧ 𝛃) ≡ (¬𝛂 ∨ ¬𝛃)
¬ (𝛂 ∨ 𝛃) ≡ (¬𝛂 ∧ ¬𝛃)

 Distributivity:
(𝛂 ∧ (𝛃 ∨ 𝛄)) ≡ ((𝛂 ∧ 𝛃) ∨ (𝛂 ∧ 𝛄))
(𝛂 ∨ (𝛃 ∧ 𝛄)) ≡ ((𝛂 ∨ 𝛃) ∧ (𝛂 ∨ 𝛄))

25 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020

 Proof: From ¬B1,1 Derive ¬P2,1

1 ¬ B1,1 Given

2 B1,1 ⇔ (P1,2 ∨ P2,1) Wumpus constraint (given)

3 (B1,1 ⇒ (P1,2 ∨ P2,1)) ∧ Biconditional elimination from 2

((P1,2 ∨ P2,1) ⇒ B1,1)

4 (P1,2 ∨ P2,1) ⇒ B1,1 And-Elimination from 3

5 ¬B1,1 ⇒ ¬(P1,2 ∨ P2,1) Contrapositive from 4

6 ¬ (P1,2 ∨ P2,1) Modus ponens from 1 + 5

7 (¬P1,2 ∧ ¬P2,1) De Morgan from 6

8 ¬P2,1 And-Elimination from 7
26 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020
 Soundness and Completeness

 Entailment: 𝛂 ⊧ 𝛃 means 𝛃 is true in all models of

𝛂.
 Derivation: 𝛂 ⊦I 𝛃 means 𝛃 can be derived from
𝛂 using the inference rules in I.

 Soundness of I: if 𝛂 ⊦I 𝛃 then 𝛂 ⊧ 𝛃
 Using I, we only derive entailed sentences.
 “We don’t make stuff up.”

 Completeness of I: if 𝛂 ⊧ 𝛃 then 𝛂 ⊦I 𝛃
 All entailed sentences are derivable using I.
 “If it’s true, we can deduce it.”
27 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020
 Validity and Satisfiability

 A sentence 𝛂 is valid if it is true in all models. We

denote this by ⊧𝛂.

 A sentence 𝛂 is satisfiable if it is true in at least

one model.

 If a sentence 𝛂 is valid, its negation ¬𝛂 is not

satisfiable.
 To prove 𝛂, show that ¬𝛂 is unsatisfiable.

28 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020

 Theorem Proving

 Start with axioms and givens, and apply inference

rules to derive new formulae.

 But there are O(2N) formulae in N vars!

 And most are useless.

 How can we focus on formulae relevant to

proving our goal?

29 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020

 Resolution Theorem Proving

 The good news: there is a single inference rule

that is sound, complete, and can find proofs with
reasonable efficiency.

 The bad news: it only works for problems in

conjunctive normal form.

 But any sentence can be rewritten in conjunctive

normal form.

 … but length may increase exponentially.

30 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020
 Definition: Clause

A clause is a disjunction of literals:

l1 ∨ l 2 ∨ … ∨ ln

The li may be positive or negative.

A single literal l is called a unit clause.

31 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020

 Definition: Conjunctive Normal Form

A sentence is in conjunctive normal form if it is

a conjunction of clauses:
c1 ∧ c2 ∧ … ∧ cm

Example:

(P ∨ ¬Q ∨ R) ∧ (Q ∨ S) ∧ (P ∨ ¬R ∨ T)

32 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020

 Converting to CNF

B1,1 ⇔ (P1,2 ∨ P2,1) Given

(B1,1 ⇒ (P1,2 ∨ P2,1)) ∧ Biconditional elimination

((P1,2 ∨ P2,1) ⇒ B1,1)

(¬B1,1 ∨ P1,2 ∨ P2,1) ∧ Implication elimination

(twice)
(¬(P1,2 ∨ P2,1) ∨ B1,1)

(¬B1,1 ∨ P1,2 ∨ P2,1) ∧

De Morgan
((¬P1,2 ∧ ¬P2,1) ∨ B1,1)

[ (¬B1,1 ∨ P1,2 ∨ P2,1) ∧

Distributivity
(¬P1,2 ∨ B1,1 ) ∧
33 (¬P2,1 ∨ B1,1) ] Nguyen Van Vinh – UET,Result is in CNF.
VNU Hanoi 5/4/2020
 Converting to CNF

(a ∧ b) ∨ (c ∧ d) ∨ (e ∧ f) This sentence
happens to be in
DNF.

converts to

(a ∨ c ∨ e) ∧ (a ∨ c ∨ f) ∧
(a ∨ d ∨ e) ∧ (a ∨ d ∨ f) ∧
(b ∨ c ∨ e) ∧ (b ∨ c ∨ f) ∧
(b ∨ d ∨ e) ∧ (b ∨ d ∨ f) ∧
34 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020
 The Resolution Inference Rule

l1 ∨ l2 ∨ … ∨ lk , m1 ∨ m2 ∨ … ∨ mn
________________________________________________________

l1 ∨ … ∨ li-1 ∨ li+1 ∨ … ∨ lk ∨
m1 ∨ … ∨ mj-1 ∨ mj+1 ∨ … ∨ mn

where li and mj are complementary literals,

i.e., li is ¬mj.

From two clauses of length k and n, derives a new

clause of length k+n-2.

35 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020

 Resolution Example

P1,1 ∨ P2,2 ∨ P3,1 , ¬P2,2

________________________________________

P1,1 ∨ P3,1

36 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020

 Contradictions Generate
An Empty Clause

 P ∧ ¬P is a contradiction, and therefore

unsatisfiable.

 Resolving P with ¬P yields an empty clause.

P , ¬P
_____________________
⃞

37 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020

 Wumpus Reasoning by Resolution

Not a horn
clause

Tautology
(useless)

To prove ¬P1,2, add P1,2 to the set of givens and use

resolution to derive a contradiction.

38 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020

 More Efficient Inference

 Resolution is complete, but even with only one

inference rule, the worst case cost is exponential
in the # of symbols.

 But for problems that can be formulated using

Horn clauses, inference can be more efficient.

 With definite clauses entailment can be

decided in linear time.

39 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020

 Summary

 Propositional logic is a constraint language.

 Model checking can be tractable if you can exploit

locality in the state space.

 Propositional entailment is co-NP Complete, so

worst case is O(2N).

 In practice, many problems can be solved efficiently

by resolution, especially if they can be formulated
using definite clauses.
40 Nguyen Van Vinh – UET, VNU Hanoi 5/4/2020