Transcript Lecture Notes

The Semantic Web –
WEEK 8: An automatic
Proof technique..
You are here!
The “Layer Cake” Model –
[From Rector & Horrocks
Semantic Web cuurse]
Recap
• For
agents to reason, negotiate etc in the Semantic
Web environment they need to represent knowledge
and do automated inference.
•Logic is good at representing conceptual
knowledge AND reasoning with it.
•Laws of Inference are methods for deducing wffs.
They are SOUND if they only ever deduce wffs
that also logically follow.
•Modus Ponens and Modus Tollens are good
inference rules for Natural Deduction
The Semantic Web
Example Revisited
“Every student is an academic. Everybody who teaches an
academic is an academic. Jeff teaches Fred who is a student.”
What can we say about the statement “Jeff is an academic”
Translate to FOL:
S = student, D = academic, T = teaches
1. Ax S(x)=>D(x) 2. Ax (Ey T(x,y) & D(y)) => D(x)
3. S(Fred) 4. T(Jeff,Fred) Goal: D(Jeff) ?
Proof:
1+3 using Modus Ponens:
|- D(Fred)
4+D(Fred) using &-introduction:
|- T(Jeff,Fred)&D(Fred)
2+T(Jeff,Fred)&D(Fred) using Modus Ponens++ :
|- D(Jeff)
BUT this is not very good for AUTOMATED deduction
The Semantic Web
Proof by Contradiction
(Reductio ad Absurdum)
This is a very common way of reasoning - we assume
what we are trying to prove is FALSE, then get a
CONTRADICTION
=> what we were trying to prove is TRUE.
Imagine we know Wff1 to be TRUE and we want to prove
Wff2 logically follows from Wff1. If we can derive a
contradicition from
(Wff1 & ~Wff2)
then assuming Wff1 is TRUE we know
Wff1 |- Wff2
The Semantic Web
Resolution Refutation
Resolution is a super law of inference which
(a) can easily be automated
(b) when used in refutation mode it is COMPLETE - it
can deduce any Wff that logically follows.
Resolution Refutation: To PROVE Wff2 FROM Wff1
1. Translate Wff1 to CLAUSAL FORM
2. Translate ~ Wff2 to CLAUSAL FORM
3. Get contradiction from 1 + 2 using Resolution
…. If follows that Wff1 |- Wff2
The Semantic Web
CLAUSAL FORM - SOME JARGON



A LITERAL is a predicate which may be
negated, called a negative literal, or a
predicate itself, called a positive literal.
A CLAUSE is a disjunction of literals which
contain only universally quantified variables.
Sometimes we think of a clause as a SET of
literals implicitly disjuncted.
A set of wffs w1, w2, ... wn is in CLAUSAL
FORM if each wi (i=1 to n) is a clause
The Semantic Web
To change any Wff to Clausal Form:
Those Eight Steps ……..
1. Replace any occurrences of <=> using the law:
A <=> B = (A => B) & (A <= B)
2. Replace all occurrences of => and <= using the laws:
A => B = ~A v B …and... A <= B = A v ~B
3. Reduce the scope of every “~” so that they all operate on predicates. To
do this use you may need the laws:
~(Ax wff) = Ex (~wff) and ~(Ex wff) = Ax (~wff) etc
4. Standardise variables - make sure all quantified variables are different
5. Eliminate existential quantifiers - change into Skolem Constants
6. Universal quantifiers can now all be removed, making every variable
implicitly universally quantified.
7. Use the laws to convert to conjunctions of disjunctive literals
(A & B) V C = (AVC) & (B V C)
8. Making all the conjunctions implicit, we are left with a set of clauses.
The Semantic Web
Unification - substition
The law of resolution depends on the idea of “unification”. This is like
(but much more general than) the technique of ‘matching’ in Haskell
(cf PLS module). We first introduce the idea of substitution:
A legal substitution is the consistent replacing of a variable symbol x
by a term T on condition that T does not contain any occurrence of
x. If W is either is a clause we may write:
W[T/x]
meaning perform the textual substitution T for x throughout W, or
W/S
meaning perform the following sequence of substitutions on W:
S = { [T1/x1], ..., [Tn/xn]}.
[cf Reduction in Lambda Calculus in PLS module ]
The Semantic Web
Unification - definition
A set of literals unify if and only if each literal in the set is identical or a
step by step application of a sequence of legal substitutions make
them identical. Identical here means:
- they all have the same predicate symbol;
- they all have the same polarity;
- they all have the same number of slots;
- they all have identical terms in corresponding slots.
Given a set of literals we can try to UNIFY them by applying
substitutions systematically
The Semantic Web
The Law of (Binary) Resolution
Two PARENT clauses w1 and w2 infer a CHILD clause
wr if there are literals L in w1 and M in w2 such that
{L,~M} unify under some substitution sequence S.
we can deduce
wr = [ w1 U w2 -- { L, ~ M } ]/S.
The law also assumes that each clause has unique variable letters. This
does not restrict its generality because variables in separate clauses are
independent.
The Semantic Web
Example
S = student, D = academic, T = teaches
Ax S(x)=>D(x) ;
Ax (Ey T(x,y) & D(y)) => D(x)
S(Fred) ; T(Jeff,Fred)
Goal: D(Jeff)
CLAUSAL FORM of Wff1 & ~Wff2:
1. ~S(x) V D(x)
2. ~T(x,y) V ~D(y) V D(x)
3. S(Fred)
4. T(Jeff,Fred)
5. ~D(Jeff)
The Semantic Web
Example
1. ~S(x) V D(x)
3. S(Fred)
Subs = Fred / x
D(Fred)
2. ~T(x,y) V ~D(y) V D(x)
Subs = Fred / y
5. ~D(Jeff)
~T(x,Fred) V D(x)
Subs = Jeff / x
~T(Jeff,Fred)
4. T(Jeff,Fred)
..So D(Jeff) follows from our premises
The Semantic Web
Summary
Resolution is a law of inference that is based on:
- Wffs in CLAUSAL FORM
- The method of UNIFICATION of literals
Resolution Refutation is a deduction procedure
that is

COMPLETE

amenable to AUTOMATION
The Semantic Web