In the introduction to first order logical notation and conventions used, I was strongly reminded of Sussmanâs Structure and Interpretation of Classical Mechanicsâs thesis: That lisp function definitions are daylight to the benighted blackboard sigils that show you are part of the club that can write (hypothetically, read) this stuff.
The background thrust of the chapter seems to be that if you wanted to recreate lisp software at institutions or companies with non-lisp language affiliations, this chapter gives enough contextual commentary for you to kind-of do so for logic processing.
Fortunately, that gradually and reluctantly gives way to a quite interesting treatise on this piece of the history of lisp over the course of the major topic treated in the chapter; automatic theorem provers.
The chapter rolls very dryly through a bunch of theorem proofs about what an automatic theorem prover could be like.
The theorems are like the theorem that if your automatic theorem prover rewrites expressions, it should not infinitely loop like (a * b) = (b * a) = (a * b) = ... or that it must not go off on endless tangents like x = x + 0 = x + 0 + 0 = x + 0 + 0 + 0 .... I guess these proofs are chosen to follow from the logic-notation-for-beginners section while also being on topic. The topic alternates into vague commentary on ideas that sound good but are found to be exponential complexity and hence impossibly slow in the big-O sense, though they donât introduce big-O as the notation.
My dominant thought while looking at the proofs that certain transformations did not cause certain infinite loops was as I mentioned, that the chapter badly needed a rewrite to be like Sussmanâs SICM in which the historical notation and convention was just thrown away and replaced with the modern historical lisp notation and convention.
(Aside: What I just said was basically Sandewallâs idea with the AICA volumes he wrote 2010-2014 see here)
However, short initial references to Boyer, Moore and Kaufmann turn up, and increasing references to John McCarthyâs creation and early articles of the subject begin appearing.
The industrial-grade, very widely used in software and hardware verification (their words), 2005 ACM software award winning ACL2 theorem prover (Nqthm theorem prover now industrial-strength) basically puts the topic to rest, and questions the usefulness of their grab bag of features that a new one would probably want to have if you wrote your own one not in lisp (no infinite loops!).
They do eventually refer those trying to implement a new one to The Handbook of Automatic Provers instead. They should have done that a lot earlier, and directed practical readers to ACL2âs famous case study with Mitsubishi, and elided much of this section.
But as I mentioned, once they finally accepted LISP as their guiding light, the chapter really comes into its own. Honestly, I didnât know that Boyer and Moore developed their provers directly as a response to McCarthyâs initial article suggesting mechanical theorem proving (getting into McCarthyâs famous reasoning-about-airplanes and things).
After going through the main chapter body which was on automatic theorem prover implementation, they share the consensus that the way automatic theorem provers, a big success, apparently must work is not a good fit for real-time logicist AI (i.e. the Knowledge Representation/KR people) because it takes a long time to automatically find proofs, even though those proofs are basically worth it in different contexts, and further that automatic provers basically must be an expert system with a human operator dynamically responding to its successful lemmas and failures. The human expert and very-very-long-run-time natures of automatic proving of first order logic are not the crisis-decision-making technology the KR people crave.
Higher order logics are talked about, largely in terms of what they lose and why they are so unreasonably hard to program towards compared to first order logic automatic theorem provers like the 2005 ACM prize-winning ACL2.
Here we get to Cyc. Cyc is not doing automatic theorem proving though it sort of looks like it does. The grab-bag-of-tricks approach to implementing fast and effective theorem proving I guess evolved into not-actually-doing-theorem-proving but instead basically doing tricks which, if they were going to work, worked in more-or-less real time (five orders of magnitude faster at creating the same logical answer to âcan babies be doctors?â compared to a major automatic theorem prover logical AI.
I guess a decade after the book, Cyc was eventually stopped and given up. However the common-lisp powered ACL2 is going strong today. ACL2 is extremely active both academically and industrially here in 2025, by the way https://acl2.org/ .
Prolog gets some discussion as the-most-popular-logic-language. However, expressing some apparently straightforward ideas in prologâs horn clause logic is prohibitively hard, and also designing theories that the prolog search algorithm is going to play nicely with requires enormously specific knowledge of how the prolog search interprets the logic and was implemented.
(Though I would point out that ACL2 needs a comparable level of what-exactly-it-is-that-ACL2-does-automatically knowledge to work with; but the vast majority of writing ACL2 is, in the pure lisp logical tradition exactly the same as host common lisp in the first place so you already know how to write everything that is not a theorem).
As I mentioned, the rest of the chapter is basically notes on lisp history, with the logicist AI (the book is on team logicist AI) and anti-logicist-AI (McDermott after changing teams, Minsky) clashes illustrating the Yale Shooting Problem (where without an additional rule for causality, logically shooting someone with a loaded gun has funny degenerate logical solutions), nonmonotonic logics (not claiming to have universal knowledge of facts) and so forth. This is very good. I wish it wasnât tucked behind the introduction to logic at the start of the chapter.
They do note that cheap and fast statistical strategies done in mass had taken over in natural language processing and that KR. Hang on, let me quote here directly for clarity since I want to comment.
In general, this pattern appears in other applications. Statistical learning techniques do well with low cost on relatively easy problems. However, hard problems remain resistant to these techniques. For these problems, logicist-KR-based techniques appear to work best.
Which I think is a coherent and clear acknowledgement of the translation and voice-to-text natural language processing deep learning dominance that applies exactly as written to the deep learning large models of today, about a decade after the book. The large model chat and image generating products today are a shocking party trick in the context of sufficiently easy goals that fail ubiquitously at non-extremely-easy tasks, as the book predicted. (And the chatbot vendors famously mix logicist AI into the chatbot results as the book suggested, as seen in the âchatbots that can do cryptographyâ business product, where it turned out a logicist AI product was the one adding the cryptography to the chatbotâs natural language banalities).