Transcript Resolution and NonMonotonic Reasoning

CIT 856 – Artificial Intelligence
Resolution and NonMonotonic
Reasoning
Powered by DeSiaMore
1
Making Deductive Inferences
• Knowledge
– That and, or are commutative, distributive
– Some commonly used propositional equivalence rules
• Double negation, rules [E1], [E4], [E5], de Morgans law
– Some commonly used implication rules
• Unit resolution, and elimination, or introduction,
• Existential elimination, etc.
– I tend to supply inference rules in exams
• Not simple/common ones
– Different ways of chaining together inference steps
• Forward/backward chaining, proof by contradiction
Powered by DeSiaMore
2
Making Deductive Inferences
• Understanding
–
–
–
–
What it means for two sentences to be logically equivalent
What it means for a sentence to be false
What it means for one sentence to entail another
How rewrite rules can be used for proving equivalences
• Abilities
– Use truth tables to
• Show equivalences, tautologies, that a statement is false
• That one statement implies another
– Apply inference rules
• Show what’s above and below the line
– Translate sentences:
• Be fluent in rewriting sentences
Powered by DeSiaMore
3
The Resolution Method
• Knowledge
–
–
–
–
What conjunctive normal form is
What a substitution is, what unification does
Overview of the unification algorithm
The resolution rule
• Unit resolution, full resolution, generalised resolution
• Understanding
– That resolution is refutation-complete
– Why we need conjunctive normal form/unification
– Why the occurs-check is important in unification
Powered by DeSiaMore
4
The Resolution Method
• Abilities
– Translate something into conjunctive normal form
• By using equivalence rules
• Organising quantifiers, standardising variables, etc.
• Existential elimination
– Put a constant in place of an existential variable
– Not using full skolemisation (we skipped over that)
– Prepare a set of sentences for use in a resolution proof
• Needs all sentences as single clauses (just split them)
– Find a unifying set of substitutions
• Apply them to unify two sentences
Powered by DeSiaMore
5
Resolution Theorem Proving
• Knowledge
–
–
–
–
Specifying a problem as axioms and theorem
As a search problem: operators, initial states (CNF), the goal test
Dealing with equality (demodulation)
Heuristic strategies:
• Unit preference, set of support, input resolution, subsumption
– Overview of some other topics
• Higher order proving, interactive, etc.
• Understanding
–
–
–
–
Why deriving the empty clause means a contradiction
Why we negate the theorem statement
Why proof by contradiction is valid
Know that resolution has been applied to mathematics
Powered by DeSiaMore
6
Resolution Theorem Proving
• Abilities:
– Prove a theorem using the resolution method
•
•
•
•
Remember to negate theorem statement
Follow proof all the way
Draw the proof tree
Or organise the resolution steps in a way
– Which makes me think you know what you’re doing
– Deduce something from a set of axioms
• Not necessarily related to proving something
Powered by DeSiaMore
7
Non-monotonic reasoning
• Classical logic is monotonic in the following sense: whenever a sentence A
is a logical consequence of a set of sentences T, then A is also a
consequence of an arbitrary superset of T.
• Non-monotonic reasoning:
– Additional information may invalidate conclusions.
– Non-monotonic reasoning is closer to (human) common-sense reasoning.
– Most rules in common-sense reasoning only hold with exceptions (i.e.
university_professors_teach)
• Important approaches to formalise non-monotonic reasoning:
– Default-Logics: Non-classical inference rules are use to represent defaults
– The modal approach: Modal operators are used to explicitly declare if
something is believed in or is consistent.
– Circumscription: Validity can be restricted to specific models.
– Conditional approaches: A conditional junctor is used to represent defaults in
a logical language.
Powered by DeSiaMore
8
Additional Information
Powered by DeSiaMore
9
Inference Process
Inference in formal logic is the process of
generating new wffs from existing wffs through
the application of rules of inference.
Powered by
10DeSiaMore
Inference Process
Conclusion:
• Many English sentences are ambiguous.
• There is often a choice of ways of
representing the knowledge.
• Even in very simple situations a set of
sentences is unlikely to contain all the
information necessary to reason about the
topic at hand.
Powered by
11DeSiaMore
Inference Process
Logical Inferences
Modus ponens and modus tolens provide the
foundation for making references.
Modus ponens: ((p  q) p) q
If someone is snorkeling then he is wet
"x snorkeling(X)  wet(X)
If we are given that alex is snorkeling
snorkeling (alex)
we can infer wet(alex)
Powered by
12DeSiaMore
Inference Process
Logical Inferences
Modus tolens: ((p  q) q)  p
If someone is snorkeling then he is wet
"x snorkeling(X)  wet(X)
If we are given that alex is not wet
 wet(alex)
we can infer  snorkeling(alex)
Powered by
13DeSiaMore
Inference Process
There are three reasoning methods that can be
applied to a set of premises.
1. Deduction
2. Abduction
3. Induction
Powered by
14DeSiaMore
Inference Process
Deduction is reasoning from known (premises) to
unknown (logical conclusions).
"x, "y, "z larger(x, y)  larger(y, z)  larger(x, z)
If our list of axioms contain the axioms
larger(house, car)
larger(car, cat)
Through deductive reasoning the wff
larger(house, cat)
Can be derived and added to our list of axioms
Powered by
15DeSiaMore
Inference Process
In Abduction we begin with a conclusion and procede
to derive conditions that would make the conclusion
valid. In other words we try to find an explanation
for the conclusion
It does not guarantee that a true conclusion results.
Therefore it s called unsound rule of inference.
If given A  B and B is true
Abduction allows us to say A is possibly true.
Reasoning under uncertainty.
Powered by
16DeSiaMore
Inference Process
Induction
Inductive reasoning forms the basis of scientific discovery.
If given p(a) is true
p(b) is true ……..
Then we conclude "x, p(x) is true
If we observe alex over a period of time and note that whenever he
is wet, it turns out that he has gone snorkeling.
We might induce that
"x, wet(x) snorkeling(x)
Like abduction, induction is also an unsound inference method.
Powered by
17DeSiaMore
Inference Process
Monotonic vs non-monotonic reasoning
Deductive reasoning is a monotonic reasoning that produce as
arguments that preserve truth.
Axioms are not allowed to change, since once a fact is known to be
true, it is always true and can never be modified or retracted.
Most real life problems are non-monotonic
quarter(fourth)
leading(bucks)
"Team [leading(Team)  quarter(fourth)] strategy(Team,
conservative)
We can deduce strategy(bucks, conservative)
What if the state changes to
leading(dolphins)
Powered by
18DeSiaMore
Inference Process
RESOLUTION attempts to show that the negation of the
statement produces a contradiction with the known
statements.
winter V summer
~winter V cold
 deduce
summer V cold
In the above example if it is winter the first statement is true if not
the second statement is true. From these two we can deduce
the third statement to be
trueby19DeSiaMore
Powered
Inference Process
Conjuctive normal form(Davis, 1960)
The steps to convert to conjuctive normal form:
1. Eliminate by using the fact that a  b is equivalent
to ~a V b
2. Reduce the scope of ~
~(A V B) = ~A B ~(A  B) = ~A V B
DeMorgan's law
~"x P(x) = $x ~P(x)
~$x P(x) = "x ~P(x)
Powered by
20DeSiaMore
Inference Process
3. Standardize variables so that each quantifier
binds a unique variable.
"x P(x) V "x Q(x) would be converted to
"x P(x) V "y Q(y)
4. Move all quantifiers to the left of the formula
without changing their relative order.
"x "y P(x) V Q(y)
Powered by
21DeSiaMore
Inference Process
5. Eliminate existential quantifiers. A formula
that contains an existentially quantified
variable asserts that there is a value that can
be substituted for the variable that makes the
formula true.
$y President(y)
President(S1)
can be transformed into
Powered by
22DeSiaMore
Inference Process
5. If existential quantifiers occur within the scope of a
universal quantifier then the value that satisfies the
predicate may depend on the values of the
universally quantified variables.
"x $y fatherof(y, x)
fatherof(S2(x), x)
can be transformed into "x
These generated functions are called Skolem
functions.
Powered by
23DeSiaMore
Inference Process
6. Drop the prefix.
7. Convert the matrix into conjunction of
disjuncts.
8. Call each conjunct a separate clause.
Powered by
24DeSiaMore
Inference Process
The Unification Algorithm:
The object of the unification procedure is to
discover at least one substitution that causes
two literals to match.
Powered by
25DeSiaMore
Inference Process
Example:
1. Marcus was a man.
man(marcus)
2. Marcus was a Pompeian.
pompeian(marcus)
3. All Pompeians were Romans.
"x pompeian(X)  roman(X)
4. Caesar is a ruler.
ruler(caesar)
Powered by
26DeSiaMore
Inference Process
5. All Romans were either loyal to Caesar or hated him.
"x roman(X)  loyalto(X, casear) v hate(X,
casear)
6. Everyone is loyal to someone.
"X $Y loyalto(X, Y)
7. People only try to assassinate rulers they are not
loyal to.
"X "Y person(X) ruler(Y) tryassassinate(X,Y)
~loyalto(X, Y)
8. Marcus tried to assassinate Caesar.
tryassassinate(marcus, caesar)
Powered by
27DeSiaMore
Inference Process
Proof by resolution:
Given the axioms in clause form:
1. man(Marcus)
2. Pompeian(Marcus)
3. ~Pompeian(x1) V Roman(x1)
4. ruler(Caesar)
5. ~Roman(x2) V loyalto(x2, Caesar) V hate(x2, Caesar)
6. loyalto(x3, f1(x3))
7. ~person(x4) V ~ruler(y1) V ~tryassassinate(x4, y1) V
~loyalto(x4, y1)
8. tryassassinate(Marcus, Caesar)
Powered by
28DeSiaMore
Inference Process
Prove: hate(Marcus, Caesar)
Powered by
29DeSiaMore
Inference Process
Prove: loyalto(Marcus, Caesar)
Powered by
30DeSiaMore
Inference Process
Prove: loyalto(Marcus, Caesar) - Continue
Suppose our knowledge base contained the two additional statements
9. persecute(x, y)  hate(y, x) ~persecute(x5, y2) V hate(y2, x5)
10. hate(x, y)  persecute(y, x)
~hate(x6, y3) V persecute(y3, x6)
Powered by
31DeSiaMore
Solution from Question 5
Powered by DeSiaMore
32
1. Show how to use backward chaining, forward chaining for the
following example and construct an Inference Tree
Here is an example involving an investment decision: whether to invest in IBM
stock. The following varibles are used: A= Have $10,000, B= Younger
than 30, C = Education at college level, D= Annual income of at least
$40,000, E= Invest in securities, F= Invest in growth stocks, G= Invest in
IBM stock
Each of these variables can be answered as true or false.
The facts: We assume that an investor has $10,000( A is true) and that she is
25 years old ( B is true). She would like advice on investing in IBM stock
( Yes or no for the goal).
The rules: Our knowledge base contains five rules:
•
•
•
•
•
R1: If A and C, Then E.
R2: If D and C, Then F.
R3: If B and E, Then F.
R4: If B Then C
R5: If F, Then G
Our goal is to determine whether to invest in IBM Stock.
Powered by DeSiaMore
33
Solution: Backward chaining
•
•
•
•
•
•
•
•
Start: We start by looking for a rule that includes the goal(G) in its conclusion ( THEN part).
Because, R5 is the only rule that qualifies, we start with it.
Step1: Try to accept or reject G. The ES goes to the assertion base to see whether G is there.
Since we have in the assertion base : A is true, B is true, ES proceeds to step 2
Step 2: R5 traces G to F. F is a premise of R5 is the conclusion of R2 and R3. There to check
whether F is true, we need to check either of these two rules.
Step 3: We try R2 first; if both D and C are true, then F is true. Since D is not a conclusion of
any rule, ES tries to find out the whether D is true by asking a question to the investor.
Step 4: ES does a backtracking and goes to R3: test B and E. We know that B is true because it
is a given fact. To prove E, we go to R1, where E is the conclusion.
Step 5: Examine R1. It is necessary to determine whether A and C are true.
Step 6: A is true because it is a given fact. To test C, it is necessary to test R4.
Step 7: R4 tells us that C is true. Therefore C becomes a fact . Now E is true, which validates F
which validates the goal.
Powered by DeSiaMore
34
Solution: Backward Chaining
D
and
B
C
R2
C&D
R5
R4
or
B
and
F
G
B&E
R3
A
A&C
and
E
R1
B
C
R4
Powered by DeSiaMore
35
Example 2: A person wants to fly from DSM to MWANZA and there are no direct
flights between the two cities. Therefore you try to find a chain of connecting flights
starting from DSM to MWANZA. Illustrate with backward and forward chaining.
• Backward Chaining: Start with MWANZA
• Forward Chaining: Start with DSM
Powered by DeSiaMore
36