Transcript Semantic Web - University of Huddersfield

Formal Aspects of
Computer Science - Week 5
Logic and Reasoning
Lee McCluskey, room 2/07
Email [email protected]
Recap
• Fundamental to logic languages is the idea of
INTERPRETATIONS - mapping predicates and constants to some
conceptualization of the world.
• A well formed sentence in Logic is called a Wff.
Wff2 LOGICALLY FOLLOWS from Wff1 if and only if every
interpretation that makes Wff1 true also makes Wff2 true.
Wff2 is LOGICALLY EQUIVALENT to Wff1 if and only if every
interpretation that makes Wff1 true also makes Wff2 true AND viceversa.
Logic and Reasoning in AI
Meaning of Quantifiers
Consider a Universe with individuals a,b,c,…
Ax P(x) = P(a) & P(b) & P(c) & ….
Ex P(x) = P(a) V P(b) V P(c) V ….
Ax Ay R(x,y) = R(a,a) & R(a,b) & R(a,c) &…
& R(b,a) & R(b,b) & R(b,c) & …
Ax Ey R(y,x) = Ey R(y,a) & Ey R(y,b) & Ey R(y,c) &…
=
(R(a,a) V R(b,a) V R(c,a) V …) &
(R(a,b) V R(b,b) V R(c,b) V …) &
(R(a,c) V R(b,c) V R(c,c) V …) & ….
Logic and Reasoning in AI
Meaning of Connectives
The Connectives
&, V, ~, ->, <-> , <- (NB alternative syntax =>, , <= ETC)
Get their meaning via propositional truth tables –

P
T
T
F
F
Q
T
F
F
T
PVQ
T
T
F
T
ETC
Logic and Reasoning in AI
“Laws”
These are some well known equivalent FORMS in FOL
called laws ( De Morgans laws etc)
¬(P&Q)
¬(PVQ)
P=>Q
¬¬P
PQ
etc
=
=
=
=
=
¬P V ¬Q
¬P & ¬Q
¬P V Q
P
(P=>Q)&(Q=>P)
Logic and Reasoning in AI
Quantifiers + Negation LAWS
1.
2.
¬ Ax P(x) = Ex ¬ P(x)
¬ Ex P(x) = Ax ¬ P(x)
Similary (and abstractly)
¬AE=EA¬
Logic and Reasoning in AI
Interpretations revisited
Ax Ey R(y,x)
These 2
Interpretations
SATISFY this WFF
Greater_than
Mother_of
persons
WFF =
numbers
“Given any person there is
Someone who is their mother”
WFF =
“Given any number there
Is some number greater than it”
NB Ax Ey … =/= Ey Ax
Logic and Reasoning in AI
Example
“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
Ax S(x)=>D(x)
Ax (Ey T(x,y) & D(y)) => D(x)
S(Fred) T(Jeff,Fred)
Goal: D(Jeff)
How can we get agents to automatically deduce such facts??
Logic and Reasoning in AI
Another Example
Imagine Deep Space 1 travels to Mars and observes many things about the
Martians, including the fact that some seem very hostile towards
humans. Concrete observations are as follows:
(a) All green Martians have antennae.
(b) A Martian is friendly to humans if all of its children have antennae.
(c) A Martian is green if at least one of its parents is green.
On its way back from Mars the robot is hotly pursued
by a spacecraft containing green Martians only. Should the robot
suspect it is being attacked? Or can the robot reason with its observations to
answer the question: `Are all green Martians friendly?''
and hence avert an inter-planetary conflict.
Logic and Reasoning in AI
Deduction
We deduce using sound inference rules
A Rule (Law) of Inference
 is a method for producing a new wff from
parents
 is SOUND if it only ever produces wffs that also
logically follow from the parents.
Logic and Reasoning in AI
Natural Deduction
The most famous Laws of Inference is known by
its Latin name “Modus Ponens”
From wffs OF THE FORM…
P(a)
Ax P(x)=>Q(x)
We can deduce the following Wff
Q(a)
Example: Socrates is a Man, All Men are Mortal
Deduce: Socrates is Mortal
Logic and Reasoning in AI
Natural Deduction
Another is called “Modus Tollens”
From wffs OF THE FORM…
¬Q(a)
Ax P(x)=>Q(x)
We can deduce the following Wff
¬P(a)
Example: If a thing is smoking then it is on fire.
I am not on fire.
Deduce: I am not smoking
Logic and Reasoning in AI
Unsound Deduction
Example: If a person is the murderer then that
person must have bloody hands.
The Butler has bloody hands.
Deduce: The Butler is the murderer
This is UNSOUND!!!
BH(butler)
Ax M(x)=>BH(x)
We can’t deduce anything from this!!
Logic and Reasoning in AI
One “Inference Rule” to Rule them all...
A COMPLETE proof procedure is one that,
given a wff w does follow from wff W, it will
always generate a proof.
There is a single inference rule which can be
used to create a complete proof procedure.
“You will need no other..!
It is called ....
“The Law of Resolution”
(wow)
Logic and Reasoning in AI
Automated Deduction
Automating deduction using RESOLUTION
requires Wffs to be translated to a “clausal
form”. Prolog statements are in a type of
clausal form.
The most common clausal form is when a Wff
is expressed as a set of clauses, where each
clause in the set is a disjunction of literals,
and where any variables are universally
quantified. EG
{ BH(butler),
~M(x) V BH(x) Logic} and Reasoning in AI
Summary
FOL is equipped with a form of reasoning
called deduction that can be automated
Next lecture I will cover resolution refutation, a
very efficient way to automate deduction.
Logic and Reasoning in AI