Logic in AI

Chapter 7

Mausam
(Based on slides of Dan Weld, Stuart Russell,
Subbarao Kambhampati, Dieter Fox,
Henry Kautz…)
2
 Knowledge Representation
• represent knowledge about the world in a manner that facilitates
inferencing (i.e. drawing conclusions) from knowledge.

• Example: Arithmetic logic

– x >= 5

• In AI: typically based on

– Logic
– Probability
– Logic and Probability

3
 Common KR Languages

Prop logic

Objects, Degree of Degree of

relations belief truth

Fuzzy Logic
First order predicate logic Prob. Prop. logic
(FOPC)

Time Degree of Objects,

belief relations
Facts
Objects FOPC Prob
relations FOPC
First order Temporal logic
Ontological
(FOPC)
commitment
Prob
Prop prop
facts logic logic
First order Prob. logic t/f/u Deg
Epistemological belief
commitment

4
 KR Languages
• Propositional Logic
• Predicate Calculus
• Frame Systems
• Rules with Certainty Factors
• Bayesian Belief Networks
• Influence Diagrams
• Ontologies
• Semantic Networks
• Concept Description Languages
• Non-monotonic Logic 5
 Basic Idea of Logic
• By starting with true assumptions, you can
deduce true conclusions.

6
 Truth
•Francis Bacon (1561-1626) •Blaise Pascal (1623-1662)
No pleasure is comparable to the We know the truth, not only by
standing upon the vantage-ground the reason, but also by the heart.
of truth.
•François Rabelais (c. 1490-1553)
•Thomas Henry Huxley (1825- Speak the truth and shame the
1895) Devil.
Irrationally held truths may be
more harmful than reasoned •Daniel Webster (1782-1852)
errors.
There is nothing so powerful as
truth, and often nothing so
•John Keats (1795-1821) strange.
Beauty is truth, truth beauty; that
is all ye know on earth, and all ye
need to know.
7
 Components of KR
• Syntax: defines the sentences in the language
• Semantics: defines the “meaning” to sentences
• Inference Procedure
– Algorithm
– Sound?
– Complete?
– Complexity
• Knowledge Base
8
 Knowledge bases

• Knowledge base = set of sentences in a formal language

• Declarative approach to building an agent (or other system):

– Tell it what it needs to know

• Then it can Ask itself what to do - answers should follow from the KB

• Agents can be viewed at the knowledge level

i.e., what they know, regardless of how implemented

• Or at the implementation level

i.e., data structures in KB and algorithms that manipulate them
9
 Propositional Logic
• Syntax
– Atomic sentences: P, Q, …
– Connectives:  , , , 
• Semantics
– Truth Tables
• Inference
– Modus Ponens
– Resolution
– DPLL
– GSAT

10
 Propositional Logic: Syntax
• Atoms
– P, Q, R, …
• Literals
– P, P
• Sentences
– Any literal is a sentence
– If S is a sentence
• Then (S  S) is a sentence
• Then (S  S) is a sentence
• Conveniences
P  Q same as P  Q
11
 Semantics
• Syntax: which arrangements of symbols are legal
– (Def “sentences”)
• Semantics: what the symbols mean in the world
– (Mapping between symbols and worlds)

Inference
Sentences Sentences
Semantics

Semantics
Representation

World

Facts Facts 12
 Propositional Logic: SEMANTICS

• “Interpretation” (or “possible world”)

– Assignment to each variable either T or F
– Assignment of T or F to each connective via defns

Q Q
T F T F
T T F T T T
P P
F F F F T F

PQ PQ

13
 Satisfiability, Validity, & Entailment
• S is satisfiable if it is true in some world

• S is unsatisfiable if it is false in all worlds

• S is valid if it is true in all worlds

• S1 entails S2 if wherever S1 is true S2 is also true

14
 Examples
PQ

R  R

S  (W  S)

T  T

XX
15
 Notation

}

 Implication (syntactic symbol)

 Inference
Proves: S1 |-ie S2 if `ie’ algorithm says `S2’ from S1
Entailment
= Entails: S1 |= S2 if wherever S1 is true S2 is also true

• Sound   =

• Complete =  

• (all truth & nothing but the truth) 16

=
 Reasoning Tasks
• Model finding
KB = background knowledge
S = description of problem
Show (KB  S) is satisfiable
A kind of constraint satisfaction
• Deduction
S = question
Prove that KB |= S
Two approaches:
• Rules to derive new formulas from old (inference)
• Show (KB   S) is unsatisfiable

17
 Special Syntactic Forms
• General Form:
((q r)  s))   (s  t)
• Conjunction Normal Form (CNF)
( q  r  s )  ( s   t)
Set notation: { ( q, r, s ), ( s,  t) }
empty clause () = false
• Binary clauses: 1 or 2 literals per clause
( q  r) ( s   t)
• Horn clauses: 0 or 1 positive literal per clause
( q   r  s ) ( s   t)
(qr)  s (st)  false
18
 Propositional Logic: Inference

A mechanical process for computing new sentences

1. Backward & Forward Chaining

2. Resolution (Proof by Contradiction)
3. Davis Putnam
4. WalkSat

19
 Inference 1: Forward Chaining

Forward Chaining
Based on rule of modus ponens
If know P1, …, Pn & know (P1 ...  Pn )  Q
Then can conclude Q

Backward Chaining: search

start from the query and go backwards

20
 Analysis
• Sound?
• Complete?
Can you prove
{ } |= Q  Q

• If KB has only Horn clauses & query is a single literal

– Forward Chaining is complete
– Runs linear in the size of the KB

21
Example

2 2

22
Example

1 1

23
Example

1 0

24
Example

1 0

25
Example

1 0

26
Example

1 0

27
Example

1 0

28
Example

0 0

29
Example

0 0

30
 Propositional Logic: Inference
A mechanical process for computing new sentences

1. Backward & Forward Chaining

2. Resolution (Proof by Contradiction)
3. GSAT
4. Davis Putnam

31
Conversion to CNF

32
 Inference 2: Resolution
[Robinson 1965]

{ (p  ), ( p    ) } |-R (    )

Correctness
If S1 |-R S2 then S1 |= S2
Refutation Completeness:
If S is unsatisfiable then S |-R ()

33
Resolution subsumes Modus Ponens

A  B, A |= B

( A  B) (A)

(B)

34
If Will goes, Jane will go
~W V J
If doesn’t go, Jane will still go J V J =J
W V J
Will Jane go?
|= J?
Don’t need to use other
equivalences if we use
resolution in refutation style
~J ~W
~W V J
W V J J
 Resolution
If the unicorn is mythical, then it is immortal, but if
it is not mythical, it is a mammal. If the unicorn is
either immortal or a mammal, then it is horned.
Prove: the unicorn is horned.

( A  H) ( H) (I  H)

M = mythical (M  A) (A) (I) ( M  I)

I = immortal
A = mammal
H = horned (M) ( M)

()
36
 Search in Resolution
Idea 1: Set of
• Convert the database into clausal form Dc
Support: At least
• Negate the goal first, and then convert it into clausal one of C1 or C2
form DG
must be either
• Let D = Dc+ DG the goal clause or
• Loop a clause derived
– Select a pair of Clauses C1 and C2 from D by doing
• Different control strategies can be used to select C1 and C2
to reduce number of resolutions tries resolutions on the
– Resolve C1 and C2 to get C12 goal clause
– If C12 is empty clause, QED!! Return Success (We proved (*COMPLETE*)
the theorem; )
– D = D + C12 Idea 2: Linear
input form:
• Out of loop but no empty clause. Return “Failure” Atleast one of C1
– Finiteness is guaranteed if we make sure that: or C2 must be one
• we never resolve the same pair of clauses more than of the clauses in
once; the input KB
• we use factoring, which removes multiple copies of (*INCOMPLETE*)
literals from a clause (e.g. QVPVP => QVP)
 Model Finding
• Find assignments to variables that makes a
formula true

38
Inference 3: Model Enumeration
for (m in truth assignments){
if (m makes  true)
then return “Sat!”
}
return “Unsat!”

39
 Inference 4: DPLL
(Enumeration of Partial Models)
[Davis, Putnam, Loveland & Logemann 1962]
Version 1
dpll_1(pa){
if (pa makes F false) return false;
if (pa makes F true) return true;
choose P in F;
if (dpll_1(pa  {P=0})) return true;
return dpll_1(pa  {P=1});
}

Returns true if F is satisfiable, false otherwise

40
 DPLL Version 1

(a  b  c)
(a  ¬b)
(a  ¬c)
(¬a  c)

41
 DPLL Version 1
a
F
(a  b  c)
(a  ¬b)
(a  ¬c)
(¬a  c)

42
 DPLL Version 1
a
F
(F  b  c)
(F  ¬b)
(F  ¬c)
(T  c)

43
 DPLL Version 1
a
F
(F  F  c)
(F  T) b

(F  ¬c)
(T  c)

44
 DPLL Version 1
a
F
(F  F  F)
(F  T) b

(F  T)
c
(T  F)

45
 DPLL Version 1
a
F
F
T b

T
c
T

46
 DPLL Version 1
a
(a  b  c)
(a  ¬b) b

(a  ¬c)
c
(¬a  c)

47
 DPLL Version 1
a
(a  b  c)
b
(a  ¬b) b

(a  ¬c)
c
c
(¬a  c)

48
 DPLL as Search
• Search Space?

• Algorithm?

49
 Improving DPLL
If literal L1 is true, then clause ( L1  L2  ...) is true
If clause C1 is true, then C1  C2  C3  ... has the same
value as C2  C3  ...
Therefore: Okay to delete clauses containing true literals!
If literal L1 is false, then clause ( L1  L2  L3  ...) has
the same value as ( L2  L3  ...)
Therefore: Okay to delete shorten containing false literals!
If literal L1 is false, then clause ( L1 ) is false
Therefore: the empty clause means false!
50
 DPLL version 2
dpll_2(F, literal){
remove clauses containing literal
if (F contains no clauses)return true;
shorten clauses containing literal
if (F contains empty clause)
return false;
choose V in F;
if (dpll_2(F, V))return true;
return dpll_2(F, V);
}

51
 DPLL Version 2
a
F
(F  b  c)
(F  ¬b)
(F  ¬c)
(T  c)

52
 DPLL Version 2
a
(b  c)
(¬b)
(¬c)

53
 DPLL Version 2
a
(F  c)
(T) b

(¬c)

54
 DPLL Version 2
a
(c)
b

(¬c)

55
 DPLL Version 2
a
(F)
b

(T)
c

56
 DPLL Version 2
a
()
b

57
 Structure in Clauses
• Unit Literals (unit propagation)
A literal that appears in a singleton clause
{{b c}{c}{a b e}{d b}{e a c}}
Might as well set it true! And simplify
{{b} {a b e}{d b}}
{{d}}
• Pure Literals
– A symbol that always appears with same sign
– {{a b c}{c d e}{a b e}{d b}{e a c}}
Might as well set it true! And simplify
{{a b c} {a b e} {e a c}}
58
 In Other Words
Formula ( L)  C2  C3  ... is only true when literal L is true
Therefore: Branch immediately on unit literals!
If literal L does not appear negated in formula F , then setting
L true preserves satisfiability of F
Therefore: Branch immediately on pure literals!

May view this as adding

constraint propagation
techniques into play
59
 In Other Words
Formula ( L)  C2  C3  ... is only true when literal L is true
Therefore: Branch immediately on unit literals!
If literal L does not appear negated in formula F , then setting
L true preserves satisfiability of F
Therefore: Branch immediately on pure literals!

May view this as adding

constraint propagation
techniques into play
60
 DPLL (previous version)
Davis – Putnam – Loveland – Logemann
dpll(F, literal){
remove clauses containing literal
if (F contains no clauses) return true;
shorten clauses containing literal
if (F contains empty clause)
return false;
if (F contains a unit or pure L)
return dpll(F, L);
choose V in F;
if (dpll(F, V))return true;
return dpll(F, V);
}
61
 DPLL (for real!)
Davis – Putnam – Loveland – Logemann
dpll(F, literal){
remove clauses containing literal
if (F contains no clauses) return true;
shorten clauses containing literal
if (F contains empty clause)
return false;
if (F contains a unit or pure L)
return dpll(F, L);
choose V in F;
if (dpll(F, V))return true;
return dpll(F, V);
}
62
 DPLL (for real)
a
(a  b  c)
(a  ¬b) b c

(a  ¬c)
c
(¬a  c)

63
 DPLL (for real!)
Davis – Putnam – Loveland – Logemann
dpll(F, literal){
remove clauses containing literal
if (F contains no clauses) return true;
shorten clauses containing literal
if (F contains empty clause)
return false;
if (F contains a unit or pure L)
return dpll(F, L);
choose V in F;
if (dpll(F, V))return true;
return dpll(F, V);
}

64
 Heuristic Search in DPLL
• Heuristics are used in DPLL to select a (non-
unit, non-pure) proposition for branching

• Idea: identify a most constrained variable

– Likely to create many unit clauses
• MOM’s heuristic:
– Most occurrences in clauses of minimum length

65
 Success of DPLL
• 1962 – DPLL invented
• 1992 – 300 propositions
• 1997 – 600 propositions (satz)
• Additional techniques:
– Learning conflict clauses at backtrack points
– Randomized restarts
– 2002 (zChaff) 1,000,000 propositions – encodings
of hardware verification problems

66
 GSAT
• Local search (Hill Climbing + Random Walk) over
space of complete truth assignments
–With prob p: flip any variable in any unsatisfied clause
–With prob (1-p): flip best variable in any unsat clause
• best = one which minimizes #unsatisfied clauses

• SAT encodings of N-Queens, scheduling

• Best algorithm for random K-SAT
–Best DPLL: 700 variables
–Walksat: 100,000 variables
67
 Refining Greedy Random Walk
• Each flip
– makes some false clauses become true
– breaks some true clauses, that become false
• Suppose s1s2 by flipping x. Then:
#unsat(s2) = #unsat(s1) – make(s1,x) + break(s1,x)
• Idea 1: if a choice breaks nothing, it is very likely to
be a good move
• Idea 2: near the solution, only the break count
matters
– the make count is usually 1
 Walksat
state = random truth assignment;
while ! GoalTest(state) do
clause := random member { C | C is false in state };
for each x in clause do compute break[x];
if exists x with break[x]=0 then var := x;
else
with probability p do
var := random member { x | x is in clause };
else (probability 1-p)
var := argminx { break[x] | x is in clause };
endif
state[var] := 1 – state[var];
end
return state; Put everything inside of a restart loop.
Parameters: p, max_flips, max_runs
 Advs of WalkSAT over GSAT
• WalkSat guaranteed to make at least 1 false
clause (in random walk also)

• Number of evaluations small per move

– does not iterate over all variables
– only variables in the sampled clause