Unit2-IntroducingClausalLogic
Course: 231 Introduction to AI
Knowledge and Inference
© Alessandra Russo
• Recall basic concepts of logic
• Logical inference
Ø deduction
Ø abduction
Ø induction
• Clausal Logic
• Deductive Inference (e.g. resolution)
• Recap of SLD and SLDNF
Course: 231 Introduction to AI
© Alessandra Russo
Logic (a recap)
q Humans capable of manipulating logical information and making logical
inference
The red block is on the green block.
The green block is somewhere above the blue block.
The green block is not on the blue block.
The yellow block is on the green block or the blue block.
There is some block on the black block.
Facts
There can be only one block on another.
A block cannot be two colors at once.
Background
knowledge
q Logic is a mechanism for expressing a particular world as a knowledge base,
and computing logical consequences of a knowledge base.
on(red, green) ∧¬on(green, blue)
∃X [ block(X) ∧ on(green, X) ∧ on(X, blue) ]
on(yellow, green) ∨ on(yellow, blue)
∃X [ block(X) ∧ on(X, black) ]
block(red) ∧ block(yellow) ∧ block(blue) ∧ block(back) ∧ block(green)
∀X,Y, Z [ on(X, Y) ∧ on(Z, Y) → X = Z) ]
Unit 2 – Introducing Clausal Logic, slide 2
Course: 231 Introduction to AI
» logical entailment of a sentence from a set of sentences, given as
premises, is when the sentence is true in all interpretations that
satisfy the premises
q Propositional Logic
» propositional constants p, q, r, s, …..
» connectives ¬ , ∧ ,∨, →
© Alessandra Russo
Logic (a recap)
Syntax
» sentences ((p∧q) ∨ r) → (p∧r))
((p∧q) ∨ r) → (p∧r))i = T
» propositional interpretation pi = T, qi = F, ri = T
assigns each propositional
constant a unique true value
» interpretation of sentences is constructed from propositional
interpretation and truth tables
{p, p → q} q⊨
Unit 2 – Introducing Clausal Logic, slide 3
Course: 231 Introduction to AI
q Predicate Logic
» propositional letters raining, snowing, wet…..
» constants table, block1, block2, etc.
» variables X, X1, Y, Y1, etc.
» functions size, color, etc.
» predicates on, above, clear, block, etc.
© Alessandra Russo
Logic (a recap)
» sentences
¬block(table)
∀X block(X) ⟷ X= block1 ∨ X=block2 ∨ X= block3
∀X,Y (block(X) ∧ block(Y) ∧ size(X) = size(Y) → sameSize(X,Y))
∀X (clear(X) ⟷ (block(X) ∧ ¬∃Y on(Y, X)))
∀X,Y (on(X,Y) ⟷ (block(X) ∧ block(Y)) ∨Y= table)
» interpretation I =
Ø constants to objects in D
Ø functions to functions over D
Ø predicates to tuples over D
» an interpretation and variable assignment satisfies a sentence if given the assignment the
sentence is interpreted to be true.
» a sentence is satisfied if there is an interpretation and variable assignment that satisfy it.
Terms
Unit 2 – Introducing Clausal Logic, slide 4
Course: 231 Introduction to AI
Example: Electric Environment
© Alessandra Russo
light(l1).
light(l2).
down(s1).
up(s2).
up(s3).
ok(cb1).
ok(outside).
connectedTo(l1, w0).
connectedTo(l2,w4).
live(outside).
connectedTo(w0,w1) ← up(s2).
connectedTo(w0,w2) ← down(s2).
connectedTo(w1,w3) ←up(s1).
connectedTo(w4,w3) ←up(s3).
connectedTo(w3, w5) ← ok(cb1).
connectedTo(w5, outside) ←ok(outside).
lit(L) ←light(L), live(L), ok(L).
live(X) ←connectedTo(X,Y), live(Y).
Query: ? lit(L)
Unit 2 – Introducing Clausal Logic, slide 5
Course: 231 Introduction to AI
Computational Logic
© Alessandra Russo
Predicate Logic helps modeling human reasoning
Theory Th
Th ⊢ CTh ⊨ C
entailment inference
Make computation logical
Expresses relations between
things using logic. Programs
describe what to compute
instead of how to compute
Make logic computational
Develop practical algorithms for
a subset of logic that is
computationally tractable.
Soudness Completeness Soudness Completeness
Unit 2 – Introducing Clausal Logic, slide 6
Course: 231 Introduction to AI
Three forms of knowledge inference
© Alessandra Russo
Deductive
Reasoning from the general to reach the particular:
what follow necessarily from given premises.
Inductive
Reasoning from the specifics to reach the general:
process of deriving reliable generalisations from observations.
Abductive
Reasoning from observations to explanations:
process of using given general rules to establish causal
relationships between existing knowledge and observations.
Unit 2 – Introducing Clausal Logic, slide 7
Course: 231 Introduction to AI
Abduction
Rule
Results
Case
All beans in this bag are white
These beans are white
These beans are from this bag
© Alessandra Russo
Deduction
Rule
Case
Results
All beans in this bag are white
These beans are from this bag
These beans are white
Induction
Case
Results
Rule
These beans are from this bag
These beans are white
All beans in this bag are white
Three forms of knowledge inference
Unit 2 – Introducing Clausal Logic, slide 8
Course: 231 Introduction to AI
© Alessandra Russo
Example: Electrical Environment
light(l1).
light(l2).
down(s1).
up(s2).
up(s3).
ok(cb1).
ok(outside).
connectedTo(l1, w0).
connectedTo(l2,w4).
live(outside).
connectedTo(w0,w1) ← up(s2).
connectedTo(w0,w2) ← down(s2).
connectedTo(w1,w3) ←up(s1).
connectedTo(w4,w3) ←up(s3).
connectedTo(w3, w5) ← ok(cb1).
connectedTo(w5, outside) ←ok(outside).
lit(L) ←light(L), live(L), ok(L).
live(X) ←connectedTo(X,Y), live(Y).
Rule
Case
Results
Deduction
live(X) ← connectedTo(X,Y), live(Y).
connectedTo(w5, outside) ← ok(outside).
live(outside).
ok(outside).
live(w5)
Unit 2 – Introducing Clausal Logic, slide 9
Course: 231 Introduction to AI
© Alessandra Russo
Example: Electrical Environment
light(l1).
light(l2).
down(s1).
up(s2).
up(s3).
ok(cb1).
ok(outside).
connectedTo(l1, w0).
connectedTo(l2,w4).
live(outside).
connectedTo(w0,w1) ← up(s2).
connectedTo(w0,w2) ← down(s2).
connectedTo(w1,w3) ←up(s1).
connectedTo(w4,w3) ←up(s3).
connectedTo(w3, w5) ← ok(cb1).
connectedTo(w5, outside) ←ok(outside).
lit(L) ←light(L), live(L), ok(L).
live(X) ←connectedTo(X,Y), live(Y).
Case
Results
Rules
Inductive
ok(outside).
connected(w5, outside) ← ok(outside).
live(outside).
live(w5).
live(X) ← connectedTo(X,Y), live(Y).
Unit 2 – Introducing Clausal Logic, slide 10
Course: 231 Introduction to AI
© Alessandra Russo
Example: Electrical Environment
light(l1).
light(l2).
down(s1).
up(s2).
up(s3).
ok(cb1).
ok(outside).
connectedTo(l1, w0).
connectedTo(l2,w4).
live(outside).
connectedTo(w0,w1) ← up(s2).
connectedTo(w0,w2) ← down(s2).
connectedTo(w1,w3) ←up(s1).
connectedTo(w4,w3) ←up(s3).
connectedTo(w3, w5) ← ok(cb1).
connectedTo(w5, outside) ←ok(outside).
lit(L) ←light(L), live(L), ok(L).
live(X) ←connectedTo(X,Y), live(Y).
Rule
Results
Case
Abduction
live(X) ← connectedTo(X,Y), live(Y).
connected(w5, outside) ← ok(outside).
live(w5).
ok(outside).
live(outside).
Unit 2 – Introducing Clausal Logic, slide 11
Course: 231 Introduction to AI
Clausal Representation
• Formulae in special form
– Theory: set (conjunction) of clauses {p∨ ¬q; r; s}
– Clause: disjuction of literals p∨ ¬q
– Literal: atomic sentence or its negation p ¬q
© Alessandra Russo
(p∨q) → ¬p
¬(p∨q) ∨ ¬p
(¬p∧¬q) ∨ ¬p
(¬p∨¬p) ∧ (¬q∨¬p)
¬p ∧ (¬q∨¬p)
eliminate →
push the ¬ inwards
distribute ∨over ∧
collect terms: ¬p∨¬p gives ¬p
CNF
What about formulae in Predicate Logic?
• Every formula can be converted into a clausal theory
Unit 2 – Introducing Clausal Logic, slide 12
Course: 231 Introduction to AI
Clausal Representation
Ø Atomic sentences may have terms with variables
– Theory {p(X)∨ ¬r(a,f(b,X)) ; q(X,Y)}
• All variables are understood to be universally quantified
∀X [ (r(a,f(b,X)) → p(X))] ∧∀X, Y q(X,Y)
© Alessandra Russo
Ø Substitution θ = {v1/t1, v2/t2, v3/t3, ….}
if l is a literal, lθ is the resulting literal after substitution
θ = {X/a, Y/g(b,Z)} p(X,Y)θ = p(a, g(b,Z))
Ø A literal is ground if it contains no variables
• A literal l′ is an instance of l, if for some θ, l′ = lθ
Unit 2 – Introducing Clausal Logic, slide 13
Course: 231 Introduction to AI
Clausal Representation
• Conversion in CNF
– Skolemisation ∃X p(X) => p(c) new constant
∀X ∃Y p(X,Y) => ∀X p(X, f(X))
– Remove universal quantifiers
© Alessandra Russo
∀X(¬literate(X) →(¬write(X) ∧¬∃Y(book(Y) ∧ read(X,Y))))
¬write(X)) ∨ literate(X)
¬book(Y) ∨ ¬read(X,Y) ∨ literate(X)
∀X(literate(X) ∨ (¬write(X) ∧¬∃Y(book(Y) ∧ read(X,Y)))) eliminate →
∀X(literate(X) ∨ (¬write(X) ∧∀Y(¬(book(Y) ∧ read(X,Y))))) push the ¬ inwards
∀X(literate(X) ∨ (¬write(X) ∧∀Y(¬book(Y) ∨ ¬read(X,Y))))
∀X,Y(literate(X) ∨ (¬write(X) ∧ (¬book(Y) ∨ ¬read(X,Y)))) remove ∀ quantifier
literate(X) ∨ (¬write(X) ∧ (¬book(Y) ∨ ¬read(X,Y)))
(literate(X) ∨ ¬write(X)) ∧ (literate(X) ∨ ¬book(Y) ∨ ¬read(X,Y))) distribute∨
Unit 2 – Introducing Clausal Logic, slide 14
Course: 231 Introduction to AI
Propositional resolution
© Alessandra Russo
fg ¬fg∨c
c ¬c∨¬f ∨g
¬f ∨g f
g ¬g
[ ]
fg
fg → c
c ∧ m → b
c ∧ f → g
f
⊨ g
KB
KB ∪ {¬g} ⊨ [ ]
§ Given two clauses of the form p∨C1 and ¬p∨C2, then
C1∨C2 is the inferred clause, called resolvent.
w ∨ r ∨ q w ∨ s ∨ ¬r
w ∨ q ∨ s
resolvent
§ Resolution is refutation complete
Th ⊨ [] iff Th ⊢ []
Unit 2 – Introducing Clausal Logic, slide 15
Course: 231 Introduction to AI
Predicate logic resolution
© Alessandra Russo
Main idea: a literal (with variables) stands for all of its instances;
so we can allow to infer all such instances in principle.
§ Given two clauses of the form φ1∨C1 and ¬φ2∨C2, then
Ø rename variables so that they are distinct in the two clauses φ1 and ¬φ2
Ø for any θ such that φ1θ = φ2θ, then infer (C1∨C2)θ as resolvent clause
Ø φ1 unifies with φ2 and θ is the unifier of the two literals
on(b,c) ¬on(X,Y)∨¬green(X)∨green(Y)
¬green(b) ∨green(c)
on(a,b)
¬green(b)
[ ]
¬green(a) ∨green(b)
{X/b, Y/c} {X/a, Y/b}
¬green(c) green(a)
green(b)
on(a,b)
on(b,c)
green(a)
¬green(c)
⊨
∃X∃Y ( on(X,Y)∧
green(X)∧
¬green(Y) )
KB
Example
Unit 2 – Introducing Clausal Logic, slide 16
Course: 231 Introduction to AI
Predicate logic resolution
© Alessandra Russo
Answering queries may return unification values as well
¬plus(X,Y, Z)∨plus(succ(X),Y, succ(Z))
¬plus(1,3,V)
¬plus(2, 3, U)
{X/1, Y/3, U/succ(V), Z/V}
[ ]
{X/0, Y/3, V/succ(W), Z/W}
¬plus(0,3,W) plus(0, X, X)
{X/3, W/3}
plus(0,X,X)
plus(X,Y,Z) →plus(succ(X), Y, succ(Z)) ⊨
KB
∃U plus(2, 3, U) U = 5
✓
Unit 2 – Introducing Clausal Logic, slide 17
Course: 231 Introduction to AI
Horn Clauses
© Alessandra Russo
Particular types of clauses with at most one positive literal.
Ø definite clauses exactly one positive literals
Ø denials no positive literals
¬b1∨¬b2∨…∨¬bn∨ h
¬b1∨¬b2∨…∨¬bn
Definite clauses can be represented as rules/facts, and denials as constraints:
¬b1∨¬b2∨…∨¬bn∨ h
¬b1∨¬b2∨…∨¬bn
h ← b1, b2, …, bn (rule)
← b1, b2, …, bn (constraint)
h h (fact)
Unit 2 – Introducing Clausal Logic, slide 18
A set of definite clauses forms a knowledge based.
A query is of the form of a denial. It can also be written as the following clause,
where X1, …, Xn are the variables occurring in the body literals:
ask(X1,…,Xn) ← b1, b2, …, bn (query)
Course: 231 Introduction to AI
SLD derivation
© Alessandra Russo
SLD inference rule
← ϕ1,…ϕn ϕ1’← β1,…, βn
← β1θ,…, βnθ, ϕ2θ,…,ϕnθ
where θ is the mgu(ϕ1, ϕ1’)
ϕi and βj are atoms
G0 ⇒ G1
C0
Gn-1 ⇒ Gn
Cn-1
…
SLD derivation
Given a denial (goal) G0 and a KB of definite clauses, an SLD-derivation
of G0 from KB is a (possibly infinite) sequence of denials
where Gi+1 is derived directly from Gi and a clause Ci in the KB with
variables appropriately renamed.
The composition θ = θ1θ2 θn of mgus, defined in each step, gives the
substitution computed by the whole derivation.
…
Unit 2 – Introducing Clausal Logic, slide 19
Course: 231 Introduction to AI
Example of SLD derivation
© Alessandra Russo
proud(X) ← parent(X,Y), newborn(Y)
parent(X,Y) ← father(X,Y)
parent(X,Y) ← mother(X,Y)
father(adam, mary).
newborn(mary).
⊨ ∃Z. proud(Z)
KB
← proud(Z) proud(X0) ← parent(X0,Y0), newborn(Y0)
← parent(Z,Y0), newborn(Y0)
{X0/Z}
C1
parent(X1,Y1) ← father(X1,Y1) C2
G0
G1
{X1/Z, Y1/Y0}
← father(Z,Y0), newborn(Y0)G2 father(adam, mary) C3
{Z/adam, Y0/mary}
← newborn(mary)G3 newborn(mary) C4
[ ]
Unit 2 – Introducing Clausal Logic, slide 20
Course: 231 Introduction to AI
SLD Trees
© Alessandra Russo
A denial can unify with more than one clause. So multiple SLD
derivations could be computed:
← proud(Z)
← parent(Z,Y0), newborn(Y0)
{X0/Z}
{X1/Z, Y1/Y0}
← mother(Z,Y0), newborn(Y0) ← father(Z,Y0), newborn(Y0)
{Z/adam, Y0/mary}
← newborn(mary)
[ ]
∎
Unit 2 – Introducing Clausal Logic, slide 21
Course: 231 Introduction to AI
Normal Clausal Logic
© Alessandra Russo
It extends Horn Clauses by permitting atoms in the body of rules or in
the denials to be prefixed with a special operator not (read as “fail”).
§ not operator is the \+ used in Prolog.
§ computational meaning of not p
§ not p succeeds if and only if p fails finitely
§ not p fails if and only if p succeeds
h ← b1, …, bn , not bn+1, …, not bm
← b1, b2, …, bn, not bn+1, …, not bm Normal denials
Normal clauses
§ fundamental constraint:
when executing not p, p must be ground
Unit 2 – Introducing Clausal Logic, slide 22
Course: 231 Introduction to AI
SLDNF derivation
© Alessandra Russo
We omit a formal definition of an SLDNF derivation
connected ← not unconnected
unconnected ← node(X),
not succ(X)
succ(X) ← arc(X,Y)
node(a)
node(b)
arc(a, b)
arc(b, c)
⊨ connected
KB
← connected
← not unconnected
← node(X), not succ(X)
← arc(a,Y)
[ ]
← succ(a)
{X/b}
← not succ(b)
← arc(b,Y)
[ ]
← succ(b)
← unconnected
succeeds
fails
← not succ(a)
{X/a}
Unit 2 – Introducing Clausal Logic, slide 23
Course: 231 Introduction to AI
SLDNF derivation
© Alessandra Russo
We omit a formal definition of an SLDNF derivation.
connected ← not unconnected
unconnected ← node(X),
not arc(X,Y)
succ(X) ← arc(X,Y)
node(a)
node(b)
arc(a, b)
arc(b, c)
⊨ connected
KB
← connected
← not unconnected
← node(X), not arc(X,Y)
{X/b}
← not arc(b,Y)
← unconnected
← not arc(a,Y)
{X/a}
floundered
floundered floundered
Any floundered branch in a tree
containing no success branch
(refutation) must flounder the node
in the parent tree
Unit 2 – Introducing Clausal Logic, slide 24
Course: 231 Introduction to AI
Summary
© Alessandra Russo
Ø Propositional and predicate logic.
Ø Types of formal reasoning:
deduction, abduction and induction
Ø Resolution: one of the main deductive proof
procedures used in computational logic.
Ø Recap of Horn clauses and SLD resolution.
Ø Illustration of SLDNF for normal clauses
Unit 2 – Introducing Clausal Logic, slide 25