CM3112 Artificial Intelligence
Propositional logic Inference
Steven Schockaert
SchockaertS1@cardiff.ac.uk
School of Computer Science & Informatics Cardiff University
Entailment
A formula β is entailed by a formula α if every model of α is also a model of β
We write this as α ⊧ β
If β is entailed by α we also say that β is a logical consequence of α
It can be shown that β is entailed by α iff α➝β is a tautology iff α∧¬β is unsatisfiable
If both α ⊧ β and β ⊧ α we say that α and β are equivalent. We write this as α≣β
Entailment: example α = a∨b
β = (a∨c)∧(b∨¬c)
Does it hold that α ⊧ β?
a
b
cα
a∨c
b∨¬c
β
false false false false true true true true
false false true true false false true true
false true false true false true false true
Enumerate all interpretations
Entailment: example
α = a∨b
β = (a∨c)∧(b∨¬c)
Does it hold that α ⊧ β?
a
b
cα
a∨c
b∨¬c
β
false false false false true true true true
false false true true false false true true
false true false true false true false true
false false true true true true true true
false true false true true true true true
true false true true true false true true
false false false true true false true true
Check which interpretations are models of α and of β
KB = {breeze(1, 2) pit(1, 1) ⇥ pit(1, 3) ⇥ pit(2, 2) pit(2, 1) breeze(1, 1),
Knowledgbereebzea(s1e, 2s), ¬breeze(1, 1)} = ¬pit(2, 1)
A knowledge base typically consists of a set of formulas, which is 1 ⇥…⇥ n ⇥x
interpreted as a conjunction of formulas
⇥ ⇥…⇥⇥ ⇥¬x 1m
In practice, available knowledge usually consists of a combination of
‣ Generic knowledge: general beliefs about the world the agent lives in
‣ Factual knowledge: corresponding to observations made by the agent 1 ⇥…⇥ n ⇥⇥1 ⇥…⇥⇥m
generic knowledge: if there is a breeze in a grid cell, there is a pit in one of its adjacent cells
KB = {breeze(1, 2) pit(1, 1) ⇥ pit(1, 3) ⇥ pit(2, 2), …, breeze(1, 2), ¬breeze(1, 1)}
2 = ¬pit(2, 2)
Factual knowledge: where have we encountered a breeze?
⇥1 ⇥…⇥⇥m ⇥¬x
1 ⇥…⇥ n ⇥⇥1 ⇥…⇥⇥m Knowledge bases
KB = {breeze(1, 2) pit(1, 1) ⇥ pit(1, 3) ⇥ pit(2, 2), …, breeze(1, 2), ¬breeze(1, 1)}
1 = ¬pit(2, 1)
Is it safe to go to cell (2,1)?
➡ Check whether KB ⊧ α1
2
1
2
1
1
(a)
KB
2
1
123
α1
2
PIT
123
123
2
1
2
1
1
123
PIT
PIT
123
PIT
PIT
2
1
2
1
PIT
123
PIT
PIT
PIT
PIT
PIT
123
123
PIT
r
r
rr
r
r
r
r
e
e
e
e
e
e
e
e
B
B
B
BB
B
B
B
e
ee
e
e
e
e
e
z
z
z
z
z
z
z
z
e
e
e
e
e
e
e
e
⇥1 ⇥…⇥⇥m ⇥¬x
1 ⇥…⇥ n ⇥⇥1 ⇥…⇥⇥m Knowledge bases
KB = {breeze(1, 2) pit(1, 1) ⇥ pit(1, 3) ⇥ pit(2, 2), …, breeze(1, 2), ¬breeze(1, 1)}
2 = ¬pit(2, 2)
Is it safe to go to cell (2,2)?
1
➡2 Check whether KB ⊧ α2
2 PIT
KB
2 PIT
2
1
PIT
123
2
1 PIT
1 2 3 α1
2
1
2
1
α
123
2
1
123
KB
2
1
123
2
1
2
1
123
2 PIT
123 1 123
2
1
PIT
PIT
123
123
2 PIT
1
PIT
1PIT 1
123 123
(a) 1 (b)
2
PIT
PIT
PIT
PIT
PIT
PIT
PIT
1 PIT 2PITPIT
123 123
PIT
1 2
123 123
PIT
PIT
PIT
r
r
rr
r
r
r
r
r
r
r
r
r
r
r
r
e
e
e
e
e
e
e
e
e
e
e
e
e
e
e
e
B
B
B
BB
B
B
B
B
B
B
BB
B
B
B
e
ee
e
e
e
eee
e
e
e
e
e
e
e
z
z
z
z
z
z
z
z
z
z
z
z
z
z
z
z
e
e
e
e
e
ee
e
e
e
e
e
e
e
e
e
Conjunctive normal form
A literal is an atom or the negation of an atom (e.g. a,¬a, …)
A clause is a disjunction of literals (e.g. a∨¬b∨c)
A formula is in conjunctive normal form (CNF) if it is a
conjunction of clauses, e.g.:
(a_¬b_c)^x^(¬a_y) Every formula is equivalent to a formula in CNF
¬¬ ⌘
¬(↵_ ) ⌘ (¬↵^¬ ) Step 1: rewrite implications
Implication law:
¬(↵^ ) ⌘ (¬↵_¬ ) (a_¬b_c)^x^(¬a_y)
↵_( 1 ^…^ n) ⌘ (↵_ 1)^…^(↵_ n) ↵! ⌘ ¬↵_
↵! ⌘ ¬↵_ ¬(a ! (b ! c)) _ d
¬(a ! (b ! c)) _ d
⌘ ¬(¬a _ (b ! c)) _ d
⌘ ¬(¬a _ (b ! c)) _ d ⌘ ¬(¬a _ ¬b _ c) _ d
⌘ ¬(¬a _ ¬b _ c) _ d ⌘ (¬¬a ^ ¬¬b ^ ¬c) _ d
( a ^ b ^ ⌘ ¬ ( c a ) ^ _ b ^d ¬ c ) _ d
⌘ (a _ d) ^ (b _ d) ^ (¬c _ d) (a_d)^(b_d)^(¬c_d)
¬¬ ⌘
⌘¬¬_¬__
¬(↵_ ) ⌘ (¬↵^¬ ) Step 2: bring negations inside
¬(↵^ ) ⌘ (¬↵_¬ ) (a_¬b_c)^x^(¬a_y)
Laws of De Morgan
↵_( 1 ^…^ n) ⌘ (↵_ 1)^…^(↵_ n) ¬(↵_ ) ⌘ (¬↵^¬ )
↵! ⌘ ¬↵_ ¬(↵^ ) ⌘ (¬↵_¬ )
¬(a ! (b ! c)) _ d
↵! ⌘ ¬↵_
⌘ ¬(¬a _ (b ! c)) _ d
⌘ ¬(¬a _ ¬b _ c) _ d
⌘ (¬¬a ^ ¬¬b ^ ¬c) _ d ¬(a ! (b ! c)) _ d
⌘ (a ^ b ^ ¬c) _ d
⌘ ¬(¬a _ (b ! c)) _ d
⌘ (a _ d) ^ (b _ d) ^ (¬c _ d) ( a b c) d
¬¬ ⌘
¬(↵_ ) ⌘ (¬↵^¬ ) Step 3: remove double negations
¬(↵^ ) ⌘ (¬↵_¬ ) (a_¬b_c)^x^(¬a_y)
Double negation
↵_( 1 ^…^ n) ⌘ (↵_ 1)^…^(↵_ n) ¬¬↵ ⌘ ↵
↵! ⌘ ¬↵_ ¬(a ! (b ! c)) _ d
¬(↵_ ) ⌘ (¬↵^¬ ) ⌘ ¬(¬a _ (b ! c)) _ d
¬(↵^ ) ⌘ (¬↵_¬ ) ⌘ ¬(¬a _ ¬b _ c) _ d
⌘ (¬¬a ^ ¬¬b ^ ¬c) _ d ⌘ (a ^ b ^ ¬c) _ d
↵_( 1 ^…^ n) ⌘ (↵_ 1)^…^(↵_ n) ⌘ (a _ d) ^ (b _ d) ^ (¬c _ d)
¬¬ ⌘ _¬_^^¬_
(a_d)^(b_d)^(¬c_d)
¬(↵_ ) ⌘ (¬↵^¬ ) Step 4: distributivity
¬(↵_ ) ⌘ (¬↵^¬ ) ¬(↵^ ) ⌘ (¬↵_¬ )
¬(↵^ ) ⌘ (¬↵_¬ )
↵_( 1 ^…^ n) ⌘ (↵_ 1)^…^(↵_ n)
↵_( 1 ^…^ n) ⌘ (↵_ 1)^…^(↵_ n) ↵! ⌘ ¬↵_
↵! ⌘ ¬↵_ ¬(a ! (b ! c)) _ d
Distributivity
⌘ ¬(¬a _ (b ! c)) _ d ¬(a ! (b ! c)) _ d
⌘ ¬(¬a _ ¬b _ c) _ d
⌘ ¬(¬a _ (b ! c)) _ d
⌘ (¬¬a ^ ¬¬b ^ ¬c) _ d ⌘ ¬(¬a _ ¬b _ c) _ d
⌘ (a ^ b ^ ¬c) _ d
( a ^⌘ b ( a ^ _ ¬ d c ) ) ^ _ ( b d _ d ) ^ ( ¬ c _ d )
eeze(1, 2) pit(1, 1) ⇥ pit(1, 3) ⇥ pit(2, 2)
pit(2 1) breeze(1 1) t
b
=
e p
t
, ,, breeze(1, 2), ¬breeze(1, 1)}
(2, 1) breeze(1, 1), reeze(1, 2), ¬breeze(1, 1)}
¬pit(2, 1)
Resolution procedure
eze(1, 2), ¬breeze(1, 1)}
it(2, 1) (2, 1)
1 ⇥…⇥ n ⇥x
(Resolution rule)
All α and β are literals, x is an atomic proposition ⇥…⇥ ⇥x
1inj
⇥…⇥ ⇥x
⇥ ⇥…⇥⇥ ⇥¬x 11nm
⇥1 ⇥…⇥⇥m ⇥¬x ⇥ ⇥…⇥⇥ ⇥¬x
1m
⇥…⇥ ⇥⇥ ⇥…⇥⇥
1n1m 1 ⇥…⇥ n ⇥⇥1 ⇥…⇥⇥m
1 ⇥…⇥ n ⇥⇥1 ⇥…⇥⇥m
1. Convert all formulas to CNF
2. Represent the knowledge base as a set of clauses (i.e. the conjuncts of the CNF formulas obtained in 1)
3. Repeatedly apply the resolution rule
Proof by refutation
Soundness: all clauses that are obtained using resolution are entailed by the knowledge base
Proving unsatisfiability: A knowledge base is unsatisfiable iff the empty clause can be derived from it using the resolution rule
Proof by refutation: To verify whether KB ⊧ α we check whether KB∪{¬α} is unsatisfiable
¬(a (b ¬c)) ⇥ d Proof by refutation
KB = {breeze(1, 2) pit(1, 1) ⇥ pit(1, 3) ⇥ pit(2, 2) pit(2, 1) breeze(1, 1),
breeze(1, 2), ¬breeze(1, 1)} = ¬pit(2, 1)
Show that KB ⊧ α using refutation
{⇥⌅⌅
Proof by refutation
pit(2, 1) ⇥ breeze(1, 1), breeze(1, 2), ¬breeze(1, 1)}
= ¬pit(2, 1)
KB ⇤ {¬ } { breeze(1, 2) ⇥ pit(1, 1) ⌅ pit(1, 3) ⌅ pit(2, 2) pit(2, 1) ⇥ breeze(1, 1),
breeze(1, 2), ¬breeze(1, 1), pit(2, 1)}
{¬breeze(1, 2) ⌅ pit(1, 1) ⌅ pit(1, 3) ⌅ pit(2, 2) ¬pit(2, 1) ⌅ breeze(1, 1),
breeze(1, 2), ¬breeze(1, 1), pit(2, 1)}
1 ⌅…⌅ n ⌅x
Convert KB⋃{¬α} to CNF ⇥1 ⌅…⌅⇥m ⌅¬x
¬⇥}
} { breeze(1, 2) ⇥ pit(1, 1) ⌅ pit(1, 3) ⌅ pit(2, 2)
{
B b
b
pit(2, 2)
¬
= ¬pit(2, 1)
breeze(1, 2), ¬breeze(1, 1), pit(2, 1)}
pit(2, 1) ⇥ breeze(1, 1),
breeze(1, 2), ¬breeze(1, 1), pit(2, 1)}
Proof by refutation
{¬breeze(1, 2) ⌅ pit(1, 1) ⌅ pit(1, 3) ⌅ pit(2, 2) ¬ } { breeze(1, 2) ⇥ pit(1, 1) ⌅ pit(1, 3) ⌅ pit(2, 2)
¬pit(2, 1) ⌅ breeze(1, 1),
{¬breeze(1, 2) ⌅ pit(1, 1) ⌅ pit(1, 3) ⌅ pit(2, 2)
pit(2, 1) ⇥ breeze(1, 1),
breeze(1, 2), ¬breeze(1, 1), pit(2, 1)}
¬pit(2, 1) ⌅ breeze(1, 1),
breeze(1, 2), ¬breeze(1, 1), pit(2, 1)}
breeze(1, 2), ¬breeze(1, 1), pit(2, 1)} ⌅…⌅ ⌅x
{¬breeze(11, 2) ⌅ pit(1n, 1) ⌅ pit(1, 3) ⌅ pit(2, 2) ⌅…⌅ ⌅x
¬pi1t(2, 1) ⌅ bnreeze(1, 1), ⇥ ⌅…⌅⇥ ⌅¬x
1m
breeze(1, 2), ¬breeze(1, 1), pit(2, 1)}
⇥1 ⌅…⌅⇥m ⌅¬x
⌅…⌅ ⌅⇥ ⌅…⌅⇥
11nn1m ⌅…⌅ ⌅x
1 ⌅…⌅ n ⌅⇥1 ⌅…⌅⇥m ⇥ ⌅…⌅⇥ ⌅¬x
1m
= {breeze(1, 2) ⇥ pit(1, 1) ⌅ pit(1, 3) ⌅ pit(2, 2), …,
reeze(1, 2) ⇥ pit(1, 1) ⌅ pit(1, 3) ⌅ pit(2, 2), …, breeze(1, 2), ¬breeze(1, 1)}
Derive new clauses using resolution
⌅…⌅ ⌅⇥ ⌅…⌅⇥ 1n1m
reeze(1, 2), ¬breeze(1, 1)} = pit(2, 2)
B b
b
pit(2, 2)
¬
⇥ ⇧…⇧⇥ ⇧¬x
¬ ¬⇥}
pit(2, 1) ⇥ breeze(1, 1), } { breeze(1, 2) ⇥ pit(1, 1) ⌅ pit(1, 3) ⌅ pit(2, 2)
{
2 1
2
= ¬pit(2, 1)
breeze(1, 2), ¬breeze(1, 1), pit(2, 1)}
breeze(1, 2), ¬breeze(1, 1), pit( {¬breeze(1, 2) ⌅ pit(1, 1) ⌅ pit(1, 3) ⌅ pit(2, 2)
pit(2, 1) ⇥ breeze(1, 1),
breeze(1, 2), ¬breeze(1, 1), pit(2, 1)}
Proof by refutation
{¬breeze(1, 2) ⌅ pit(1, 1) ⌅ pit( KB ⌅ {¬ } { breeze(1, 2) ⇥ pit(1, 1) ⇧ pit(1, 3) ⇧ pit(2, 2)
¬ } { breeze(1, 2) ⇥ pit(1, 1) ⌅ pit(1, 3) ⌅ pit(2, 2)
¬pit(2, 1) ⌅ breeze(1, 1),
{¬breeze(1, 2) ⌅ pit(1, 1) ⌅ pit(1, 3) ⌅ pit(2, 2)
pit(2, 1) ⇥ breeze(1, 1), pit(2, 1) ⇥ breeze(1, 1),
breeze(1, 2), ¬breeze(1, 1), pit(2,b1re)e}ze(1, 2), ¬breeze(1, 1), pit( ¬pit(2, 1) ⌅ breeze(1, 1),
breeze(1, 2), ¬breeze(1, 1), pit(2, 1)} breeze(1, 2), ¬breeze(1, 1), pit(2, 1)}
¬pit(2, 1) ⌅ breeze(1, 1),
breeze(1, 2), ¬breeze(1, 1), pit(2, 1)}
⌅…⌅ ⌅x 1 n
⌅…⌅ ⌅x
{¬breeze(11, 2) ⌅{¬pbitr(e1en,z1e)(⌅1,p2it)(⇧1, 3p)it⌅(1p,i1t()2⇧, 2)pit(1, 3) ⇧ pit(2, 2)
⌅…⌅ ⌅x ¬pi1t(2, 1) ⌅ bnreeze(1, 1),
¬pit(2, 1) ⇧ breeze(1, 1),
⇥ ⌅…⌅⇥ ⌅¬x 1m
⇥ ⌅…⌅⇥ ⌅¬x 1m
breeze(1, 2), ¬breeze(1, 1), pit(2, 1)}
breeze(1, 2), ¬breeze(1, 1), pit(2, 1)}
⇥1 ⌅…⌅⇥m ⌅¬x
⌅…⌅ ⌅⇥ ⌅…⌅⇥
1 ⌅…⌅ n ⌅⇥1 ⌅…⌅⇥m ⇥ ⌅…⌅⇥ ⌅¬KxB={breeze(1,2)⇥pit(1,1)⌅pit(1,3)⌅
11nn1m ⌅…⌅ ⌅x
1 ⌅…⌅ n ⌅⇥1 ⌅…⌅⇥m ⇤ 1m
= {breeze(1, 2) ⇥ pit(1, 1) ⌅ pit(1, 3) ⌅ pit(2, 2), …, Since we were able to derive the empty
reeze(1, 2) ⇥ pit(1, 1) ⌅ pit(1, 3) ⌅ pit(2, 2), …, breeze(1, 2), ¬breeze(1, 1)}
breeze(1, 2), ¬breeze(1, 1)} 1n
⇧…⇧ ⇧x
clause ⊥, it must be the case that KB ⊧ α ⌅…⌅ ⌅⇥ ⌅…⌅⇥
1 n 1 =m¬pit(2, 2) reeze(1, 2), ¬breeze(1, 1)} 2
= pit(2, 2)
Example
Use refutation to show that K ⊧ α, with:
K = {¬a → (b → c), ¬x → (¬y ∨ z), b ∧ y, ¬c ∨ s, ¬(z ∧ s)} α=a∨x
Example
Use refutation to show that K ⊧ α, with:
K = {¬a → (b → c), ¬x → (¬y ∨ z), b ∧ y, ¬c ∨ s, ¬(z ∧ s)} α=a∨x
K ∪ {¬α} = {¬a → (b → c),¬x → (¬y ∨ z),b ∧ y, ¬c∨s,¬(z∧s),¬(a∨x)}
Example
Use refutation to show that K ⊧ α, with:
K = {¬a → (b → c), ¬x → (¬y ∨ z), b ∧ y, ¬c ∨ s, ¬(z ∧ s)} α=a∨x
K ∪ {¬α} = {¬a → (b → c),¬x → (¬y ∨ z),b ∧ y, ¬c∨s,¬(z∧s),¬(a∨x)}
K ∪ { ¬α} = {a ∨ ¬b ∨ c, x ∨ ¬y ∨ z, b, y, ¬c∨s,¬z∨¬s,¬a,¬x}
Example
K ∪ {¬α} = {a ∨ ¬b ∨ c, x ∨ ¬y ∨ z, b, y, ¬c ∨ s, ¬z ∨ ¬s, ¬a, ¬x} ¬b∨c
Example
K ∪ {¬α} = {a ∨ ¬b ∨ c, x ∨ ¬y ∨ z, b, y, ¬c ∨ s, ¬z ∨ ¬s, ¬a, ¬x}
¬b∨c c
Example
K ∪ {¬α} = {a ∨ ¬b ∨ c, x ∨ ¬y ∨ z, b, y, ¬c ∨ s, ¬z ∨ ¬s, ¬a, ¬x} ¬b∨c
c s
Example
K ∪ {¬α} = {a ∨ ¬b ∨ c, x ∨ ¬y ∨ z, b, y, ¬c ∨ s, ¬z ∨ ¬s, ¬a, ¬x} ¬b∨c
c s ¬z
Example
K ∪ {¬α} = {a ∨ ¬b ∨ c, x ∨ ¬y ∨ z, b, y, ¬c ∨ s, ¬z ∨ ¬s, ¬a, ¬x} ¬b∨c
c s ¬z
x∨¬y
Example
K ∪ {¬α} = {a ∨ ¬b ∨ c, x ∨ ¬y ∨ z, b, y, ¬c ∨ s, ¬z ∨ ¬s, ¬a, ¬x} ¬b∨c
c s ¬z
x∨¬y ¬y
Example
K ∪ {¬α} = {a ∨ ¬b ∨ c, x ∨ ¬y ∨ z, b, y, ¬c ∨ s, ¬z ∨ ¬s, ¬a, ¬x} ¬b∨c
c s ¬z
x∨¬y ¬y
SAT solvers
Automated reasoners for propositional logic are often based on resolution, but naive implementation may lead to exponentially many clauses being derived
Systems which perform satisfiability checking are called SAT solvers
SAT solvers are of key importance in many areas of computer science ‣ Checking correctness of hardware and software
‣ Combinatorial design: cryptography, drug design and testing, etc. ‣ Most sub-areas of AI
SAT solvers
http://www.satcompetition.org
SAT solvers