Transcript Constraint propagation

Automated reasoning
and theorem proving
Introduction: logic in AI
Automated reasoning:
Resolution
Unification
Normalization
Introduction:
Motivating example
Automated reasoning
Logic:
Syntax
Model semantics
Logical entailment
The AI dream in the 60’s:
 Logic allows to express almost everything
‘formally’.
 Logic also allows to prove “theorems” based on the
information given.
 Can we exploit this to build automated reasoning
systems ??
3
Underlying premises:
 Logic is the ‘assembly language’ of knowledge
and is closely related to natural language.
In logic almost all kinds of knowledge can be
represented formally and unambiguously.
Since computers are supposed to process the
knowledge, it should be expressed
formally and unambiguously.
Logical deduction allows us to derive
systematically new knowledge from the
existing one.
Automating deduction ??
4
Example:
 The following knowledge is given :
1. Marcus was a man.
2. Marcus was a Pompeian.
3. All Pompeians were Romans.
4. Caesar was a ruler.
5. All Romans were either loyal to Caesar or hated him.
6. Everyone is loyal to someone.
7. People only try to assassinate rulers to whom they are not
loyal.
8. Marcus tried to assassinate Caesar.
 Can we automatically answer the following questions?
 Was Marcus loyal to Caesar?
 Did Marcus hate Caesar?
5
Conversion to
the First Order Logic:
 Representation of facts:
1. Marcus was a man.
man(Marcus)
2. Marcus was a Pompeian.
Pompeian(Marcus)
4. Caesar was a ruler.
ruler(Caesar)
8. Marcus tried to assassinate Caesar.
try_assassinate(Marcus, Caesar)
6
Conversion to
the First Order Logic (2):
 General representation (representation of rules):
3. All Pompeians were Romans.
x Pompeian(x)  Roman(x)
5. All Romans were either loyal to Caesar or hated him.
x Roman(x)  ( loyal_to(x,Caesar)  hates(x,Caesar) ) 
~(loyal_to(x,Caesar)  hates(x,Caesar))
XOR
6. Everyone is loyal to someone.
x y loyal_to(x,y)
7. People only try to assassinate rulers to whom they are not
loyal.
xy person(x)  ruler(y)  try_assassinate(x,y) 
~loyal_to(x,y)
7
The “theorem” ?
Was Marcus loyal to Caesar?
Try, for example, to prove that he was not :
~loyal_to(Marcus,Caesar)
Did Marcus hate Caesar?
Prove that he did:
hates(Marcus,Caesar)
8
A proof using backwardreasoning problem-reduction:
~loyal_to(Marcus,Caesar)
xy person(x)  ruler(y) 
try_assassinate(x,y)  ~loyal_to(x,y)
+ substitution: x/Marcus
y/Caesar
person(Marcus)  ruler(Caesar)  try_assassinate(Marcus,Caesar)  ~loyal_to(Marcus,Caesar)
AND
+ Modus ponens
person(Marcus)
try_assassinate(Marcus, Caesar)
Extra rule:
x man(x)
 person(x)
man(Marcus)
1.
ruler(Cesar)
Done!
4.
8.
Done!
Done!
9
Problems:
1) knowledge representation:
 Natural language is imprecise / ambiguous
 see “People only try …”
 Obvious information is easily forgotten.
 see man <-> person
 Some information is more difficult to represent in
logic.
 Vb.: “perhaps …”, “possibly…”, “probably…”,
“the chance of … is 45%”,
 Logic is inconvenient from a software
engineering perspective.
 too ‘fine-grained’ (like an assembly language)
10
Problems:
2) Problem solving:
 All trade-offs that we had with search methods
based on states space representation:
 backward/forward, tree/graph, OR-tree/AND-OR,
control aspects, ...
 What deduction rules are needed in general?
 Example: prove “ hates(Marcus,Caesar) “
The only applicable rule is:
x Roman(x)  loyal_to(x,Caesar)  hates(x,Caesar)
Modus ponens???
 How do we handle x and y ?
11
Problems:
2) Problem solving (2):
 How to compute substitutions in the general case ?
xy person(x)  ruler(y) 
try_assassinate(x,y)  ~loyal_to(x,y)
In general:
more complex
+ substitution: x/Marcus
y/Caesar
 Which theorem do we try to prove?
 Ex.: loyal_to(Marcus,Caesar) or ~loyal_to(Marcus,Caesar)
 How to handle equality of objects?
 Problem: combinatorial explosion of the derived
equalities (reflexivity, symmetry, transitivity, …)
 How to guarantee correctness/completeness?
12
The formal model semantics
of Logic
The meaning of “Logical entailment”
Semantics / Logical
entailment:
 Given a set of formulas S:
a model is an interpretation that makes all
formulas in S true.
 Given a set of formulas S and a formula F:
F is logically entailed by S ( S |= F ), if
all models of S also make F true.
 Additional: inconsistency:
 Given a set of formulas S:
S is inconsistent if S has no models.
Example: S = { p(a), ~p(a)}
14
Marcus example:
Marcus
C
y
x
ruler
V
A
F=
Caesar
P
man person
Pompeian try_assassinate
Roman
loyal_to
hates
“Intended” interpretation:
D = world of ~40 VC.
“Caesar”
true
Boolean
“Marcus”
“was_pompeian”
“was_ruler”
true
false
Boolean
false
Is a model IF ALL FORMULAS ARE CORRECT
15
Marcus example:
Marcus
C
x
y
A
V
F=
Caesar
P
man person ruler
Pompeian try_assassinate
Roman
loyal_to
hates
N
3
4
I(man) = I(person)= I(Roman)
= “natural number”
I(try_assassinate) = “ > ”
I(Pompeian) = “even number”
I(loyal_to) = “divides”
I(ruler) = “prime number”
I(hates) = “doesn’t divide”
16
Model ??
YES !
1. Marcus was a man.
4 is a natural number
2. Marcus was Pompeian.
4 is an even number
4. Caesar was a ruler.
3 is a prime number
8. Marcus tried to
assassinate Caesar. 4 > 3
3. All Pompeians were Romans.
Even numbers are naturals.
5. All Romans were either loyal to Caesar or hated him.
A number either divides 3 or doesn’t divide 3.
6. Everybody is loyal to somebody.
Each number is a divisor of some number.
7. People try to assassinate only those rulers to whom they
are not loyal. A natural number that is greater than a
prime number doesn’t divide the prime number.
17
“Logic is all form, no content”
person(x)  mortal(x)
person(Socrates)
January(x)  cold(x)
January(21/1/01)
P(x)  Q(x)
P(A)
mortal(Socrates)
cold(21/1/01)
Q(A)
Only the underlying structure of a set of logical formulas is
important for the conclusions! (up to the names isomorphism)
But from the knowledge representation perspective
also the ‘contents’ is important.
18