Transcript Wed 22nd Apr

Inference and Reasoning
Basic Idea
• Given a set of statements, does a new
statement logically follow from this.
• For example If an animal has wings and it
has feathers- we can conclude that it is a
bird since this logically follows from our
premises.
We have already seen this
• In expert systems we had backward and
forward chaining.
• Based on our set of rules we concluded
that something held based on the chain of
rules that followed from our initial facts.
In logic
• There are two main kinds of inference
• 1: Term rewriting
• 2: Resolution.
• Both start with an initial set of statements
and try to show that the hypothesis or new
statement is consistent with the existing
set.
Consistency
• Recall our definitions of satisfaction
Satisfaction
•
•
A predicate calculus expressions S1 is satisfied.
Definition If there exists an Interpretation I and a
variable assignment under I which returns a value T
for S1 then S1 is said to be satisfied under I.
•
•
A set of predicate calculus expressions S is satisfied.
Definition For any interpretation I and variable
assignment where a value T is returned for every
element in S the the set S is said to be satisfied,
Consistency
• Given a set of statements S and a new
statement S1
• Then for any interpretation I and variable
assignment where set S is satisfied, if S1
is also assigned T under I and the same
variable assignment then S1 is said to be
consistent with S under this interpretation
and variable assignment.
Term Rewriting
• In logic there are many valid statements that is
statements that are true under any Interpretation
and variable assignment
•
•
•
•
•
Sometimes these are called tautologies
Many are based around equivalences
For example the law of the double negative
 (A) = A
These truths are sometimes called the laws of
logic
Examples of these Laws of logic
•
•
•
•
•
•
•
Modus Ponens
A B == A  B, 
De Morgans Laws
(A  B) == A   B
(A  B) == A   B
Or Reduction
A  T = T, A  F = A ,A   A = T
More Examples of these Laws of
logic
•
•
•
•
•
•
•
•
And Reduction
A  T = A, A  F = F ,A   A = F
Commutativity
A  B == B  A
A  B == B  A
Distribution
A  (B  C) = (A  B)  (A  C)
A  (B  C) = (A  B)  (A  C)
Laws around Quantifiers
• x y is the same as y x
•
• x y is the same as y x
•
• x y is not the same as y x
•
• x y Loves(x,y)
– “There is a person who loves everyone in the world”
–
• y x Loves(x,y)
– “Everyone in the world is loved by at least one person”
–
• Quantifier duality: each can be expressed using the other
•
• x Likes(x,IceCream)
x Likes(x,IceCream)
Term Rewriting
• This shows that a new sentence is
consistent with the existing set of
sentences by showing it is equivalent to a
sentence that is known to be true
• It does this by replacing sub-phrases of
existing sentences by equivalences
defined by the laws of logic
Term rewriting example
• To show that
• Given
•  (A  B)  B is T Prove that A is either T or F
using Term Rewriting
•  (A  B)  B ==  (A  B)  B
• Modus Ponens
• From De Morgans
•  (A  B)  B ==  ( A)   B  B
• From law of Double Negation
•  ( A)   B  B == A   B  B
Continued
• A   B  B == A  T from Laws of OR
reduction and Finally
• A  T = T also from Laws of OR reduction
whether A is T or F QED
Another example of Term Rewriting
• Conversion to Clause form
• See attached Document
Resolution
• Another approach to Inference is
Resolution due to Robinson
• Resolution works on the principle of Proof
By Refutation
Proof by Refutation
• In order to show that a statement S1 is
consistent with a set of statements S take
 S1(i.e refute S1) and show that  S1 is
inconsistent with S.
• If  S1 is inconsistent with S then it follows
that S1 must be consistent.
• Proof by refutation turns an important
property of inference on its head.
Semi -Decidability
• In the theory of computation Inference(Theorem
Proving) has been shown to be a semi decidable
process.
• That is we can show that something is not
consistent with our set of premises (“decide”)but
we cannot guarantee demonstrating its
consistency
• That is why resolution tries to show
inconsistency (which can be guaranteed to be
shown) of the refutation
Resolution
• Resolution theorem proving works by showing the
negation of the theorem, to be proved cannot be true.
This is called proof by refutation.
• To use resolution, the axioms involved in the proof must
be expressed in a logic form called clause form.
•
Logic sentences in clause form contain no quantifiers,
implications or conjunctions.
• Clause 1:Not(Hairy(X))  Dog(X) is an example of a
sentence in clause form.
Resolvents
• Resolution theorem proving works by producing
resolvents.
• Two clauses can be resolved to produce a new
clause(i.e. its resolvent), if one clause contains
the negation of a predicate in the other formula.
• The resolvent consists of those literals in both
clauses less the opposing literals.
• The following clause
• Clause 2: Hairy(X) could be resolved with
Clause 1. to produce the resolvent Dog(X).
Unification
• It might be that two literals are not quite direct
opposites but only can be matched by
appropriate substitutions. Finding appropriate
substitutions is called unification and the
substitution is called a unifier.
• For example, if clause 2 were Hairy(Y) then it
could only be resolved with clause 1 using the
unifier {Y / X} i.e. Y substituted by X.
• To illustrate Resolution theorem proving we use
clause 1 and the latter version of clause 2, i.e.
Hairy(Y).
• The theorem we want to prove is that X is a dog,
i.e. Dog(X). So we negate this clause to
produce clause 3, Not(Dog(X)).
• Resolving clause 1 and clause 2 using the
unifier {Y/ X} we get clause 4, Dog(X). Adding
this and clause 3 to the set of clauses we get:
Set of Clauses
•
•
•
•
Clause 1:Not(Hairy(X))  Dog(X).
Clause 2:Hairy(Y).
Clause 3:Not(Dog(X).
Clause 4: Dog(X).
Inconsistency
• Now, all these clauses are supposed to be
true but we have a contradiction between
clause 3 and clause 4, so the refutation of
the theorem, i.e. clause 3 is inconsistent
with the original set of clauses. Therefore
we can assume the theorem to be proved.
Another Example
•
•
•
•
•
•
•
•
•
Given the following set of clauses use resolution to
prove the axiom : expensive(f1car)
1: fast(X)  big(X)
2:  big(Y)  economical(Y)  showy(f1car)
3:  fast(U)  new(U)
4:  showy(T)  high_tax(T)
5:  new(G)
6:  high_tax(S)
7:  economical(Z)  expensive(Z)
(8 marks)
• To Prove expensive(f1car)
• ADD 8:  expensive(f1car)
•
•
•
•
•
•
•
•
•
Set of Clauses Now
1: fast(X)  big(X)
2:  big(Y)  economical(Y)  showy(f1car)
3:  fast(U)  new(U)
4:  showy(T)  high_tax(T)
5:  new(G)
6:  high_tax(S)
7:  economical(Z)  expensive(Z)
8:  expensive(f1car)
Resolve
• Resolve
• 1: fast(X)  big(X) with
• 2:  big(Y)  economical(Y) 
showy(f1car)
• with {X/Y} to get
• 9: fast(X)  economical(X)  showy(f1car)
Resolve
• Resolve
• 9: fast(X)  economical(X)  showy(f1car)
with
• 3:  fast(U)  new(U)
• with {X/U} to get
• 10 economical(X)  showy(f1car) 
new(X)
Resolve
• Resolve
• 10 economical(X)  showy(f1car) 
new(X)
• with
• 5:  new(G)
• with {X/G} to get
• 11 economical(X)  showy(f1car)
Resolve
•
•
•
•
Resolve
11 economical(X)  showy(f1car)
with
7:  economical(Z)  expensive(Z) with
{X/Z} to get
• 12 showy(f1car)  expensive(X)
Resolve
•
•
•
•
•
•
Resolve
12 showy(f1car)  expensive(X)
With
8:  expensive(f1car)
with {f1car/X} to get
13 showy(f1car)
Resolve
•
•
•
•
•
Resolve
13 showy(f1car) With
4:  showy(T)  high_tax(T)
With {f1car/T} to get
14 high_tax(f1car)
Resolve
•
•
•
•
•
Resolve
14 high_tax(f1car) with
6:  high_tax(S)
With {f1car/S} to get
15 [] QED
Unification
• Note in the above example we made many
substitutions
• This was done by a process of legal
substitutions called legal substitutions
which will be described in the following.
An algorithm for performing
unification
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
Function Unify(E1, E2);
begin
case
both E1 and E2 are constants or the empty list
if E1 = E2 then return {} else return FAIL
E1 is a variable: if E1 occurs in E2 then return FAIL
else return {E2/E1};
E2 is a variable: if E2 occurs in E1 then return FAIL
else return {E1/E2};
otherwise
begin
HE1:= head of E1
HE2:= head of E2
SUBS1 = UNIFY(HE1,HE2);
IF SUBS1 = FAIL THEN RETURN FAIL;
TE1 := APPLY( SUBS1, REST OF E1)
TE2 := APPLY( SUBS1, REST OF E2)
SUBS2:= UNIFY(TE1,TE2);
IF SUBS2 = FAIL THEN RETURN FAIL; ELSE RETURN THE COMPOSITION OF SUBS1 AND SUBS2.
END
end end.
Example of the algorithm
•
p(X,a,Y) with p(Z,Z,b)
•
•
•
Basically the algorithm processes from left to right
including the function symbols
E1 is p(X,a,Y) in list form E1 is
(p X a Y)
•
•
E2 is p(Z,Z,b) in list form E2 is
(p Z Z b)
•
Constants in lowercase, Variables in upper
•
The algorithm starts with the head of E1 and E2
•
•
•
•
•
•
•
•
•
•
•
•
Head of E1 = p
Head of E2 = p
p = p so return nothing {}
Next apply algorithm to rest of list
Start with head of rest of list
Tail E1 = (X a Y)
Tail E2 = (Z Z b)
Head of tail E1 = ( X| a Y) = X
Head of tail E2 = ( Z |Z b) = Z
X is a variable and so is Z so according to algorithm
Appropriate substitution is
{X/Z}
•
•
Next apply algorithm to rest of list
Start with head of rest of list
•
{X/Z, a/X,bY}
•
•
•
•
•
•
•
•
•
•
Apply substitution X/Z to both tails to get
Tail E1 = (a Y)
Tail E2 = (X b)
Head of tail E1 = ( a| Y) = a
Head of tail E2 = ( X | b) = X
a is a constant and X is a variable so according to
algorithm
Appropriate substitution is
{a/X}
Next apply algorithm to rest of list
Start with head of rest of list
•
•
•
•
•
•
Apply substitution a/X to both tails to get
Tail E1 = (Y)
Tail E2 = (b)
Head of tail E1 = (Y) = Y
Head of tail E2 = ( b) = b
b is a constant and Y is a variable so according to
algorithm
• Appropriate substitution is
• {b/Y}
• Now there is nothing left on either list so we get
Our Unifier
• {X/Z, a/X,bY}
Note
• In our algorithm we have something called an
occurs check .
• We see if one expression occurs in the other.
For example if we have X in E and F(E) in
another then if we replaced E by F(E) we would
get F(E). Replacing the E in this by F(E) we get
F(F(E)) and so on ad infinitum to get
F(F(F(F…………(F(E)))))))) and still have to
make the substitution. This cannot happen so
we stop it by failing the unification on nan occurs
check.
See this in the following example
•
password( mary, favourite(Y,X)) with
password(X, favourite(toy,f(X))
•
Representing these in list form
•
•
•
•
E1 = (password mary (favourite Y Z))
E2 = (password X (favourite Y (f Z)))
Following the algorithm through this
password matches so {}
•
•
•
•
•
Next
Tail E1 = (mary (favourite Y Z))
Tail E2 = (X (favourite Y (f Z)))
Following the algorithm through this
Substitution recommended by
algorithm for mary and X is {mary/X}
• So moving on through the rest of the
lists
•
•
•
•
•
•
Tail E1 = (favourite Y Z)
Tail E2 = (favourite Y (f Z))
The next 2 steps of the algorithm see
favourite and favourite matched and
Y and Y matched
So no need for substitutions
• Next comes the problem
• Tail E1 = (Z)
• Tail E2 = ((f Z))
• We see that Z occurs in (f Z) so our
occurs check fails and we FAIL the
unification