Transcript FOL is More Powerful Than it Looks

OTTER;
Suppositional Theorem-Proving and OSCAR;
Automated Test Creation and Production
2/12/01
Logic (Programming) & AI
Selmer Bringsjord
[email protected]
www.rpi.edu/~brings
General discussion of LP
paradigm…
Recall: Two Perspectives
• Logic Programming as arising from Herbrand’s
Theorem, etc.
• Logic Programming as using a logical system (in
mathematical sense of this phrase)
• I will take second perspective, which subsumes
first
– E.g., completeness theorem for first-order logic (LI)
allows one to affirm Herbrand’s Theorem
– This theorem fully done in LCU
• What you need to know to understand second
perspective is precisely what you need to know to
understand first
The Dreadsbury Mansion Mystery
Someone who lives in Dreadsbury Mansion killed Aunt Agatha.
Agatha, the butler, and Charles live in Dreadsbury Mansion, and
are the only people who live therein. A killer always hates his
victim, and is never richer than his victim. Charles hates no one
that Aunt Agatha hates. Agatha hates everyone except the butler.
The butler hates everyone not richer than Aunt Agatha. The
Can
you get
it, prove
butler hates everyone
Agatha
hates.
No oneit?
hates everyone.
Agatha is not the butler.
Now, given the above clues, there is a bit of disagreement
between three (competent?) Norwegian detectives. Inspector
Bjorn is sure that Charles didn’t do it. Is he right? Inspector
Reidar is sure that it was a suicide. Is he right? Inspector Olaf is
sure that the butler, despite conventional wisdom, is innocent. Is
he right?
On OTTER
•
•
•
•
•
Return to Logic Theorist problems
Syllogisms in OTTER
LCU and resolution rules. Also in AIMA
Jobs puzzle and other things online…
Dreadsbury Mansion Mystery in OTTER
– My first exercise
• “Victor” Murder Mystery in OTTER
• Bird problem in OTTER (unilluminating)
Overview of OSCAR in
Connection to Natural
Deduction…
first via “Bird” Problem in
Hyperproof, then
via Pollock’s ppt file…
The Bird Problem
Is the following assertion true or false? Prove that you are correct.
There exists something which is such that if it’s a bird, then
everything is a bird.
x(B(x) yB(y))
Good litmus test for mastery of proof theory in FOL
Overview of
Intelligent Test
Creation/Production…
other ppt file