程序代写代做代考 prolog algorithm AI Unit2-IntroducingClausalLogic

Unit2-IntroducingClausalLogic

Course: 231 Introduction to AI

Knowledge and Inference

• 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

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 ¬ , ∧ ,∨, →

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.

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 = where D is a universe of discourse and i maps:
Ø 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

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

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

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

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

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

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

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

(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)

Ø 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

∀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

fg ¬fg∨c

c ¬c∨¬f ∨g

¬f ∨g f

g ¬g

[ ]

fg
fg → c
c ∧ m → b
c ∧ f → g
f

⊨ g

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

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) )

Example

Unit 2 – Introducing Clausal Logic, slide 16

Course: 231 Introduction to AI

Predicate logic resolution

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)) ⊨

∃U plus(2, 3, U) U = 5
✓

Unit 2 – Introducing Clausal Logic, slide 17

Course: 231 Introduction to AI

Horn Clauses

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

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

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)

← proud(Z) proud(X0) ← parent(X0,Y0), newborn(Y0)

← parent(Z,Y0), newborn(Y0)

{X0/Z}
C1

parent(X1,Y1) ← father(X1,Y1) C2

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

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

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

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

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

Ø 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

Related Posts