 |
| Amazon Link |
His 1979 book, Logic: Form and Function, is out of print and now only available second-hand. It's sunk into obscurity, as you can see from Amazon's terrible image above.
After some efforts, I have managed to order a copy and will do my best to write a review (Google reports no accessible reviews on the Internet). Here is some background on Robinson (Wikipedia).
"Robinson was born in Halifax, Yorkshire, England in 1930 and left for the United States in 1952 with a classics degree from Cambridge University. He studied philosophy at the University of Oregon before moving to Princeton University where he received his PhD in philosophy in 1956. He then worked at Du Pont as an operations research analyst, where he learned programming and taught himself mathematics.---
He moved to Rice University in 1961, spending his summers as a visiting researcher at the Argonne National Laboratory's Applied Mathematics Division. He moved to Syracuse University as Distinguished Professor of Logic and Computer Science in 1967 and became professor emeritus in 1993.
It was at Argonne that Robinson became interested in automated theorem proving and developed unification and the resolution principle. Resolution and unification have since been incorporated in many automated theorem-proving systems and are the basis for the inference mechanisms used in logic programming and the programming language Prolog.
Automated theorem proving (ATP) is the engine of classical AI in the way that neural nets are the engine of contemporary AI.
Deep Learning, which makes everything into a classification problem, has superseded brittle, classical AI not least because high-level features emerge from the weight-training process under some optimisation criteria, rather than being hand-crafted by the programmer.
Check this brilliant article from the NYT (via Steve Hsu).
But if your ambitions are somewhat modest, ATP takes you a long way .. and you can do it at home, kids.
---
Here is the table of contents from "Logic: Form and Function".
And finally, here is the text from Chapter 13 where Robinson documents his (very old-fashioned) Lisp code for the hyper-resolution theorem prover (PDF).
My apologies for the poor quality, but it is readable. To make sense out of how it works, I suspect you need to buy the book and to read the preceding chapters.
So one development in Logic since the GOFAI days is that Godel's Completeness Theorem (and hence most of the 1st Order Meta-Logic Theorems) are not recursively valid ("Non-algorithmic" as Penrose might say). They are all to be replaced by a new axiom called "WKL". This has had interesting effects on the Foundations of Mathematics in a research Programme called "Reverse Mathematics". One mathematical consequence is the failure of several "Fixed Point Theorems" (though not e.g. Kleene's I think) - there are many other conseqences in Mathematics. I am trying to work out further consequences in Logic (with the occasional success) and from there into AI and QM (and Economics too!).
ReplyDeleteApparently Godel expressed reservations about that Theorem in his PhD, but the reservations were deleted in the 1930 published paper - one author suggests it might have been to avoid "controversy". Interesting and puzzling...
I'm reading the "Reverse Mathematics" Wikipedia article with interest.
Delete