Transcript FOL is More Powerful Than it Looks

History of IT and AI
F03
CSD ProSem
Selmer Bringsjord
[email protected]
www.rpi.edu/~brings
What is a Proof?
• Aristotle
– Syllogisms
– Frenchmen example…
– Fatal problems (including can’t handle Euclid!)
• If Jason is in fact a financial whiz, then the Giants will win the
Superbowl. Jason is in fact a financial whiz. Therefore the
Giants will win the Superbowl.
• Minor enhancements from Stoics and Medievil
logicians
– E.g., modus ponens…
– But 2,400 yrs until real progress!
Story Continues
• Lull and his wheel (14th century)
– Check out the cover of AIMA: there’s a lot there
• Hobbes: “Thinking is calculation” (17th century)
• DesCartes: Deduction is the method; linguistic
capacity the human/animal divide
– (By Selmer’s lights, DesCartes seems to have gotten
things essentialy correct)
• And suddenly Boole appears!
Boole’s Innovation Essentially
the Propositional Calculus
• p, q, r, …
Boolean
connective

Approximate
English correlate
Not

And

Or

If …, then …

… if and only if …
Frege Answers the Question!
• First-order Logic
• Add
– variables x, y, z, …
– quantifiers  
– relation symbols R, F, G, …
• “Everyone loves someone” is xyLxy
• A proof is reasoning that can be formalized
as a step-by-step progression in first-order
logic…
And Shortly Thereafter…
• Kronecker refuses to accept Cantor’s Proof
– E.g., that the power set of the natural numbers is
“larger” than the natural numbers
• Hilbert expresses Kronecker’s attitude in his
“program”: use algorithms to answer all
mathematical questions
• Gödel obliterates Hilbert’s dream; Turing follows
suit (and actually generalizes, with a simpler
proof)
• Gödel needs precise account of computable
• Turing provides “Turing Machines”
– Out of TMs we get digital computers
– Turing not sure a physical UTM is physically possible!
• Church: “Hey, TMs, -calculus, etc. all the
same!”
Intuitive Picture of Turing Machine
And AI and Agent Tech Specifically?
• Artificial Neurons: McCulloch & Pitts
– Prop. Calc. + Turing Machines +
Neurophysiology
• Princeton
– Minsky: Neural networks
– McCarthy there as well
• Dartmouth workshop 1956
– Minsky, McCarthy, Simon, Newell, …
– Logic Theorist!
And…
• McCarthy in 1958
–
–
–
–
•
•
•
•
•
Lisp born
Advice Taker
McCarthy and Minsky clash over logic
McCarthy leaves for Stanford
Minsky and Microworlds
Minsky and Pappert kill connectionist approach
Logicist systems rule (expert systems)
Connectionism comes back
And today?
– New edition of AIMA reacts to Web
– Hybrid approaches
– ,,,