Transcript OTTER-Notes1 - COW :: Ceng On the Web

Automated Reasoning
Dr. Ferda Nur Alpaslan
Chapter 1 - Introduction
What do they have in common ?
• 12 billiard balls problem
• Missionaries and Cannibals puzzle
• Dominoes puzzle
Each can be solved with logical reasoning.
They have all been solved with the same
computer program
Logical reasoning
•
•
•
•
•
key to
solving puzzles
solving problems in mathematics
designing electronic circuits
debugging and verifying computer
programs
answering many everyday questions
Human Logic
• Fragments of Information
• The red block is on the green block.
• The green block is somewhere above the blue
block.
• The green block is not on the blue block.
• The yellow block is on the green block or the blue
block.
• There is some block on the black block.
Conclusions
•
•
•
•
•
The red block is on the green block.
The green block is on the yellow block.
The yellow block is on the blue block.
The blue block is on the black block.
The black block is directly on the table.
Proof
• We are told that the yellow block is on the
green block or the blue block. We are also
told that the red block is on the green block.
Given the assumption that there can be only
• one block on another and that a block
cannot be two colors at once,
• we can conclude that the yellow block is not
on the green block. But then, by elimination,
the yellow block must be on the blue block.
Reasoning by Pattern
• All Accords are Hondas.
• All Hondas are Japanese.
• Therefore, all Accords are Japanese.
• All borogoves are slithy toves.
• All slithy toves are mimsy.
• Therefore, all borogoves are mimsy.
• All x are y.
• All y are z.
• Therefore, all x are z.
Unsound Patterns
Pattern
• All x are y.
• Some y are z.
• Therefore, some x are z.
Good Instance
• All Toyotas are Japanese cars.
• Some Japanese cars are made in America.
• Therefore, some Toyotas are made in America.
Not-So-Good Instance
• All Toyotas are cars.
• Some cars are Porsches.
• Therefore, some Toyotas are Porsches.
Induction - Unsound
• I have seen 1000 black ravens.
• I have never seen a raven that is not black.
• Therefore, every raven is black.
Abduction - Unsound
•
•
•
•
•
•
If there is no fuel, the car will not start.
If there is no spark, the car will not start.
There is spark.
The car will not start.
Therefore, there is no fuel.
What if the car is in a vacuum chamber?
Formal Logic
1. Formal language for encoding information
2. Legal transformations
Formalization
Simple Sentences:
p: Mary loves Pat.
q: Mary loves Quincy.
m: It is Monday.
Premises:
pq:
If Mary loves pat, Mary loves Quincy.
mpq: If it Monday, Mary loves Pat or Quincy.
pq : Mary loves one person at a time.
Questions:
p : Does Mary love Pat?
q : Does Mary love Qunicy?
Rule of Inference
Propositional Resolution
NB: If pi on the left hand side of one sentence is the same as
qj in the right hand side of the other sentence, it is okay to
drop the two symbols, with the proviso that only one such
pair may be dropped.
NB: If a constant is repeated on the same side of a single
sentence, all but one of the occurrences can be deleted.
• p1  ...  pk  q1 ...  ql
• r1  ...  rm  s1 ...  sn
• p1 ...  pk  r1 ...  rm  q1 ...  ql s1 ...  sn
Logic Problem Revisited
pq
mpq
mqq
mq
• If Mary loves Pat, then Mary loves Quincy.
• If it is Monday, then Mary loves Pat or Quincy.
• If it is Monday, does Mary love Quincy?
Automated Reasoning
Goal
KB rules
Proof  KB
Goal in
Proof ?
success
YES
NO
R  chose(rules)
P  choose(proof)
Q  choose(proof)
C  apply(R,P,G)
Proof  Proof | C
What is Automated Reasoning ?
Reasoning : process of drawing conclusions
from facts.
Automated Reasoning : developing computer
programs that assist in solving problems
and in answering questions requiring
reasoning.
Formal Logic
• Syntax, semantics, correctness and completeness
• Emphasis on minimal sets of rules to simplify analysis
• These rules are not always easy to implement or efficient
Computational Logic
• Syntax, semantics, correctness, completeness
• Also concerned with efficiency
• Emphasis of different languages and different sets of rules
• Attention to those that better suited to automation
Applications
Group Axioms
• (x x y) x z = x x (y x z)
• xxe=x
• exx=x
• x x x-1 = e
Theorem:
• x-1 x x = e
Tasks:
• Proof Checking
• Proof Generation
Database Systems
Database in Tabular Form
Art
Bob
Art
Bea
Bea Coe
Database in Sentential Form
parent(art, bob)
parent(art, bea)
parent(bob,coe)
Constraints
 parent(x, x)
parent(x, y)   parent(y, x)
Definitions
parent(x, y)  parent(y,z)  grandparent(x, z)
Program Verification
Program
L
Sorter
 Sort(L)
Specification:
i. j. (i < j  sort(L)i < sort(L)j )
Tasks:
• Partial Evaluation
• Verification
• Proof of Termination
• Complexity Analysis
Hardware Engineering
Understanding the behavior of a logic circuit
Tasks:
• Partial Evaluation
• Verification
• Proof of Termination
• Complexity Analysis
Logic Technology
• Components
• Editors
• Automated Reasoning Systems
• Knowledge Bases
Some Popular Automated Reasoning Systems
• Boyer-Moore
• Otter
• PTTP
• Epilog
Multiple Logics
• Propositional Logic
If it is raining, the ground is wet.
• Relational Logic
If x is a parent of y, then y is a child of x.
• Metalevel Logic
John believes everything that Mary tells
him.
How does an automated reasoning
program reason ?
A merchant, wishing to sell you some fruit, places three boxes on a table. Each
box contains only one kind of fruit: apples, bananas, or oranges. As a gesture
of good will, the merchant, after asking you to turn your back, selects a piece
of fruit from each box and hands you a beautiful apple, a beautiful banana, and
a beautiful orange, establishing that each box contains a different type of fruit.
You are momentarily puzzled by the request to turn your back, but the reason
quickly becomes apparent. The merchant loves to gamble and offers you the
chance to win all of the fruit if you can figure out what is in each box. If you
lose, you must pay three times that it is worth. The merchant tells you
correctly that each box is mislabeled. Box a is labeled apples, box b oranges,
box c bananas. You accept the bet on the condition that you are allowed to
look in the box labeled oranges. The merchant agrees, and you look in box b
and find that it contains apples. You then turn to the merchant and announce
corretly the contents of the other two boxes, and win the fruit. How did you do
it ?
Your solution: Since box b contains apples,
box a and box c do not. Since box c is
labeled bananas, and since the label is
incorrect, box c does not contain bananas.
So, box c contains oranges, and box a
contains bananas.
Solution of an automated reasoning program:
(1) CONTAINS(b,apples).
(2) LABEL(a,apples).
(3) LABEL(b,oranges).
(4) LABEL(c,bananas).
(5) CONTAINS(a,apples) |
CONTAINS(a,bananas) |
CONTAINS(a,oranges).
(6) CONTAINS(b,apples) |
CONTAINS(b,bananas) |
CONTAINS(b,oranges).
(7) CONTAINS(c,apples) |
CONTAINS(c,bananas) |
CONTAINS(c,oranges).
(8) -CONTAINS(a,apples) | -CONTAINS (b,apples).
(9) -CONTAINS(a,apples) | -CONTAINS (c,apples).
(10) -CONTAINS(b,apples) | -CONTAINS (c,apples).
(11) -CONTAINS(a,bananas) | -CONTAINS (b,bananas).
(12) -CONTAINS(a,bananas) | -CONTAINS (c,bananas).
(13) -CONTAINS(b,bananas) | -CONTAINS (c,bananas).
(14) -CONTAINS(a,oranges) | -CONTAINS (b,oranges).
(15) -CONTAINS(a,oranges) | -CONTAINS (c,oranges).
(16) -CONTAINS(b,oranges) | -CONTAINS (c,oranges).
(17) -LABEL(x,y) | -CONTAINS(x,y).
Given statements 1-17, an automated reasoning
program can apply a rule for drawing conclusions
that would produce the following statements.
(18) -CONTAINS(c,apples). (From 1 and 10)
(19) -CONTAINS(c,bananas). (From 4 and 17)
(20) CONTAINS(c,oranges). (From 18, 19, and 7)
(21) -CONTAINS(a,apples). (From 1 and 8)
(22) -CONTAINS(a,oranges). (From 20 and 15)
(23) CONTAINS(a,bananas). (From 21, 22, and 5)
An automated reasoning program can use a
strategy that decreases its chance of getting
lost on the way to solving the puzzle.
Chapter 2 - Summary of Logic
• and, or, not, if-then
s1
T
T
F
F
s2
T
F
T
F
s1 and s2
T
F
F
F
s1
T
T
F
F
s2
T
F
T
F
s1 or s2
T
T
T
F
s1
T
F
not s1
F
T
s1
T
T
F
F
s2
T
F
T
F
if s1 then s2
T
F
T
T
A Language for Automated Reasoning
Programs
Predicates
• Kim is female
• Kim is male
• Three is less than five
• The product of a and b
is c
• Kim is not male
•
•
•
•
FEMALE(Kim).
MALE(Kim).
LESSTHAN(three,five).
PRODUCT(a,b,c).
• -MALE(Kim).
• Kim is female or male
• FEMALE(Kim) |
MALE(Kim).
• Kim is a female and a
parent
• FEMALE(Kim).
PARENT(Kim).
• Kim is younger than
Mary and (Ann is
younger than Kim or
Ann is younger than
Mary)
• YOUNGER(Kim,Mary).
YOUNGER(Ann,Kim) |
YOUNGER(Ann,Mary).
• John is older than Tom or
richer than Jim.
• OLDER(John,Tom) |
RICHER(John, Jim).
• If Jim is at home, then
Mary is not.
• ATHOME(Jim) =>
-ATHOME(Mary).
equivalent to
-ATHOME(Jim) |
-ATHOME(Mary).
• Tom is a father and happy.
• FATHER(Tom).
HAPPY(Tom).
Variables
• Kim has a child if she is a mother.
MOTHER(Kim) => HASCHILD(Kim).
-MOTHER(Kim) | HASCHILD(Kim).
• Everyone who has a child is a mother.
-MOTHER(x) | HASCHILD(x).
Functions
• Ankara begins with the letter A.
IS(first(Ankara),A).
• Two times three is six.
EQUAL(times(two,three),six).
PRODUCT(two,three,six).
• For every number, there is a number bigger than it.
-NUMBER(x) | GREATER(successor(x),x).
• -MARRIEDTO(x,y) | WIFE(x,y) | HUSBAND(x,y).
equivalent to
• -MARRIEDTO(x,y) | IS(x,wife(y)) |
IS(x,husband(y)).
• -NUMBER(x) | GREATERTHAN(successor(x),x).
can be expressed as
• GREATERTHAN(successor(x),x).
where, the universe of discourse is implicit.
And/Or Combinations, Complex if-then, and
DeMorgan’s Laws
-(s1 and s2) is logically equivalent to - s1 or - s2
• If Kim is a female and a parent, then Kim is a mother.
-FEMALE(Kim) | -PARENT(Kim) | MOTHER(Kim).
- s1 or (s2 and s3) is logically equivalent to
(- s1 or s2) and (-s1 or s3)
• If a number is divisible by 8, then the number is
divisible by 4 and by 2.
• -DIVISIBLE(x,8) | DIVISIBLE(x,4).
-DIVISIBLE(x,8) | DIVISIBLE(x,2).
s1 and (s2 or s3) is logically equivalent to
(s1 and s2) or (s1 and s3)
(need not be applied)
s1 if and only if s2 is logically equivalent to
(if s1 then s2) and (if s2 then s1)
i.e.
s1 <=> s2 is logically equivalent to
s1 => s2 and s2 => s1.
Assumptions and Axioms, Types of
Reasoning, and Proof
An automated reasoning program answers questions
(ranging from puzzles to deep mathematical
questions) by starting some set of assumptions or
axioms, applying some type of reasoning called
inference rules, and seeking an answer in the form
of a proof. The inference rules are the means for
drawing conclusions.
The knowledge given to a reasoning program at the
start of a problem are called assumptions or
axioms.
UR- Resolution
• Fact: Father and son have the same last name:
-SON(x,y) | SAMELAST(x,y).
Fact: Ali is the son of Veli:
SON(Ali,Veli).
Conclusion: Ali and Veli have the same last name:
SAMELAST(Ali,Veli).
• Fact: All numbers divisible by 4 are divisible by 2:
-DIVISIBLE(x,4) | DIVISIBLE(x,2).
Fact: The number 63 is not divisible by 2:
-DIVISIBLE(63,2).
Conclusion: 63 is not divisible by 4:
-DIVISIBLE(63,4).
Hyperresolution
• Fact: A sister and brother have the same father:
-SISTER(x,y) | -FATHER(z,y) |FATHER(z,x).
Fact: Rita is Harry’s sister:
SISTER(Rita,Harry).
Fact: George is Harry’s father:
FATHER(George,Harry).
Conclusion: George is Rita’s father:
Father(George, Rita).
• A person’s child is that person’s daughter or son:
-CHILD(x,y) | DAUGHTER(x,y) | SON(x,y).
Kim is Rita’s child:
CHILD(Kim,Rita).
therefore
Kim is Rita’s daughter or Rita’s son:
DAUGHTER(Kim,Rita) | SON(Kim,Rita).
Proof
• Fact: Harry’s father is George.
Fact: Harry’s sister is Rita.
Fact: Rita has never married.
Claim: Harry and Rita have the same last name.
How can an automated reasoning program be asked to prove
this claim ?
A very common way is to ask the program to find a
contradiction.
Translated facts:
(1) FATHER(George,Harry).
(2) SISTER(Rita,Harry).
(3) NEVERMARRIED(Rita).
We must also supply clauses that give information
about family relationships:
(4) -NEVERMARRIED(x) | -FATHER(y,x) |
SAMELAST(y,x).
(5) -SISTER(x,y) | -FATHER(z,y) |FATHER(z,x).
(6) -SAMELAST(x,y) |-SAMELAST(y,z) |
SAMELAST(x,z).
(7) -FATHER(x,y) | -MALE(y) | SON(y,x).
(8) -SON(x,y) | SAMELAST(x,y).
(9) MALE(Harry).
Finally, we translate the assumed falseness of the
claim:
(10) -SAMELAST(Harry,Rita).
which will eventually lead to a contradiction.
The proof proceeds as follows:
(11) FATHER(George,Rita).
(12) SAMELAST(George,Rita).
(13) SON(Harry,George).
(14) SAMELAST(Harry,George).
(15)-SAMELAST(George,Rita).
(16) CONTRADICTION !
from 2, 1, and 5.
from 3, 11, and 4.
from 1, 9, and 7.
from 13 and 8.
from 14,10,and 6.
from 12 and 15.
Thus, we have a proof that Harry and Rita have the
same last name.