Transcript FOL is More Powerful Than it Looks

Symbolic Logic Foundations:
An Overview
F03
CSD ProSem
Selmer Bringsjord
[email protected]
www.rpi.edu/~brings
Logic Programming: 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
Logical Systems
(Are Programming Langs in here?)
Name
Alphabet
Grammar
Proof
Theory
Semantics
Metatheory
LPC
p, q, r, … and
truthfunctional
connectives
Easy
Fitch-style and
natural
deduction
Truth tables!
Sound,
complete,
compact,
decidable
Add variables
x, y, … and 

Easy
Fitch-style and
natural
deduction
Structures and
interpretations
Sound,
complete,
compact,
undecidable
LPML
Add “box” and
“diamond” for
necessity and
possibility
Wffs created
by prefixing
new operators
to wffs
Add
necessitation,
etc.
Possible
worlds
Same as PC
LII
New variables
for predicates
Pretty obvious
New adapt
quantifier
rules
Quantification
over subsets in
domain
allowed
Sound but not
complete
Propositional Calculus
LI
First-Order Logic
Readings
•
•
•
•
AIMA
“Natural Deduction” on Pollock’s web site
OTTER manual
“Logic and AI: Divorced, Still Married…”
– http://kryten.mm.rpi.edu/COURSES/ILOGPROG/lai.ed2.pdf
• LCU
– http://www.rpi.edu/~faheyj2/SB/LCU/lcu.driver.pdf
LPC (Propositional Calculus)
• Where we left off: Logic Theorist problems
in OTTER…
• Ad lib in HYPERPROOF…
• Some problems
– NYS 1, NYS 2, NYS 3, J-L 1
• Semantics of Propositional Calculus: Truth
Tables
– Boole
– Via HYPERPROOF
– Full formal view: LCU
“NYS 1”
Given the statements
a  b
b
ca
which one of the following statements must also be true?
c
b
c
h
a
none of the above
“NYS 2”
Which one of the following statements is logically equivalent to the
following statement: “If you are not part of the solution, then you
are part of the problem.”
If you are part of the solution, then you are not part of the problem.
If you are not part of the problem, then you are part of the solution.
If you are part of the problem, then you are not part of the solution.
If you are not part of the problem, then you are not part of the
solution.
“NYS 3”
Given the statements
c
ca
a  b
bd
(d  e)
which one of the following statements must also be true?
e
c
e
h
a
all of the above
J-L 1
Suppose that the following premise is true:
If there is a king in the hand, then there is an ace
in the hand, or else if there isn’t a king in the hand,
then there is an ace.
What can you infer from this premise?
NO!
There is an ace in the hand. NO!
In fact, what you can infer is that there isn’t an ace in the hand!
Proof Theory of LI (First-order logic)
•
•
•
•
Ad lib in HYPERPROOF
Syllogisms in OTTER
Dreadsbury Mansion Mystery
The Bird Problem
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?
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
Metatheory for PC and FOL
• Soundness
– If you start with true propositions in an agent’s knowledge base, deduction from
that kb will always yield a true conclusion.
• Completeness
– If something intuitively “follows from” a given kb, then the agent can prove it
from the kb.
• Decidability & undecidability
– If Dec: There is a decision algorithm which can tell you whether a given formula
is a theorem.
• Compactness
– Not today
• Herbrand’s Theorem etc.
– Not today
• Godel’s Theorem
– Not today
• LII not complete
– Not today
• Lindstrom’s Theorems
– Already characterized intuitively at start of lecture