Pure ATPs: such a disappointment

---

I have always had a soft spot for automated theorem provers (ATPs). There is something both elegant and exciting about formalising your nontrivial problem in, say, a predicate calculus variant, then pressing the start-button and letting the machine solve it by the powers of deep deduction alone.

But ATPs have always disappointed. Doug Lenat, who spent his entire life handcrafting the general purpose intelligent system Cyc, commented at the last that they had originally encoded the facts and rules of the world in a Lisp-like formal language and then handed that knowledge base and the user-query to a powerful Resolution Theorem Prover to deduce an answer. To avoid the interminable waiting they added layer after layer of special-case heuristics. After decades of such aggregation they quietly turned off the theorem prover: it was never being used.

Edinburgh university was one of the centres of Prolog use and research in the 1980s, along with Oxford and Imperial College. Undergraduates hated it: the elegance of its specification capability was complemented by the opacity of its execution model. Debugging logic programs by mentally running a depth-first tree-search with backtracking-on-failure - well, that could tax the abstraction-powers of the keenest young minds. 

I was much happier with Lisp: you know where you are with β-reduction.

In the heady days of those applied ATPs known as Expert Systems the slogan was: “In the knowledge lies the power”; inferential capability was distinctly secondary.

The culmination of this insight was the success of the LLMs c. 2024. Enormous amounts of encoded knowledge - and no reasoning ability at all…

And yet, there are still those of us who value the elegance of inference... and now, in 2025, my happiness is complete: those LLMs can now reason!

---

Google Translate: English to predicate logic (please!)

Did you see the  "Missing: google"?

---

A big problem with English (natural language really) is that it doesn't come equipped with an explicit set of inference rules. Consequently, when someone uses natural language to communicate with an AI system, it's not really possible for that system to immediately connect the utterance to its store of knowledge. If only natural languages were like formal languages, which have proper inference and well-defined semantics. The thought that secretly they are was the intuition of Richard Montague*. But he was misguided.

Any AI natural language understanding system tries to transform the raw material of human language into something it can use, something more inferentially tractable.  Usually that doesn't work too well, and even the latest statistical systems (which do well in surface-level speech-recognition and translation) show scant abilities to understand.

It's as well to remind ourselves just why natural languages are so unhelpful to AI designers. It's because they are a highly-optimised solution to a situated communications problem. Speech is a low-bandwidth, linear and slow channel for communicating time-critical thoughts. So speech is highly optimized to use every available constraint to speed up meaning transfer:

• volume, pitch, timbre and tone of voice
• shared and predictive knowledge of the conversational partner
• emotional cues
• physical gesturing and facial expressions
• environmental situation and context 
• ...

Researchers are quite aware of this, of course. The topic area is called Pragmatics and it's hived off as a separate sub-discipline .. because it seems to require way too much modelling of the conversing agents in their specific environment, culture and history. In short, it's too hard.

But by abstracting away these additional constraints which channel and constrain meaning, we make the semantic understanding problem way too hard. Which is why we can't solve it.

A Google Translate system which mapped between a natural language and a formal language (with well-defined inference rules and semantics) would nevertheless be a boon to the designers of conversational AI systems, including chatbots. But Google doesn't have a corpus of First-Order Predicate Calculus sentences translationally-linked to English, so its deep learning systems can't crunch the data and add FOPC to its list of languages. Projects such as Cyc have attempted to do this stuff by hand .. with surprisingly little impact.

Again the way forward is embodied robotics and human baby conversational emulation.

---

* In a weird reprise of Alan Turing's fate, Wikipedia reports that Richard Montague 'died violently in his own home; the crime is unsolved to this day. Anita Feferman and Solomon Feferman argue that he usually went to bars "cruising" and bringing people home with him. On the day that he was murdered, he brought home several people "for some kind of soirée", but they instead robbed his house and strangled him.'

He was 40.

AI Progress Report

So I got 'Eliza' working today, the simplified version from 'The Art of Prolog'. Time to take stock and figure out where to go next.

First, Prolog. Its supporters always touted it as a higher-level language than Lisp - though I always found Lisp more congenial, I like to set up data structures and manipulate them explicitly. With Prolog you define relationships between things and the miraculous powers of unification and depth-first search with backtracking pull magical rabbits out of hats. The Eliza program in Prolog can be read in its entirety on one screen, ditto for the blocks world planning system.

This procedural power is the result of enormously complex recursive structures built at execution time by the Prolog system. It frequently defies one's powers of abstraction, short-term memory and inference to visualise what's actually going on. I know you're meant to read and understand the programs declaratively, but in reality you don't get too far without a consideration of what actually happens at run-time.

Still, the power to write ridiculously-powerful programs in just a few lines of code is addictive. It reminds me of the first time I fired the General-Purpose Machine Gun (GPMG). I was good with the Lee-Enfield rifle and prided myself on my accuracy; the GPMG just bounced around and hosed the target. So much power and so little control!

---

Eliza and the Blocks World Planner were little milestones I had set myself, like climbing Pen y Fan. Items on my bucket list if you like. So what next?

Once you know how to set up knowledge bases and inferential systems you have the tools for developing intelligent agents. But, as I have cited before on these pages, 'in the knowledge lies the power'. If your agent lives in a closed-world with a fixed and limited database and rule set, it's going to run out of new things to do pretty fast. The interest comes from its interactions with the wider world.

Yet as Doug Lenat noted in the context of his 'Cyc' project:

"Any time you look at any kind of real life piece of text or utterance that one human wrote or said to another human, it's filled with analogies, modal logic, belief, expectation, fear, nested modals, lots of variables and quantifiers," Lenat said. "Everyone else is looking for a free-lunch way to finesse that. Shallow chatbots show a veneer of intelligence or statistical learning from large amounts of data. Amazon and Netflix recommend books and movies very well without understanding in any way what they're doing or why someone might like something.

"It's the difference between someone who understands what they're doing and someone going through the motions of performing something."

Cycorp's product, Cyc, isn't "programmed" in the conventional sense. It's much more accurate to say it's being "taught." Lenat told us that most people think of computer programs as "procedural, [like] a flowchart," but building Cyc is "much more like educating a child."

"We're using a consistent language to build a model of the world," he said.

This means Cyc can see "the white space rather than the black space in what everyone reads and writes to each other." An author might explicitly choose certain words and sentences as he's writing, but in between the sentences are all sorts of things you expect the reader to infer; Cyc aims to make these inferences.

Consider the sentence, "John Smith robbed First National Bank and was sentenced to 30 years in prison." It leaves out the details surrounding his being caught, arrested, put on trial, and found guilty. A human would never actually go through all that detail because it's alternately boring, confusing, or insulting. You can safely assume other people know what you're talking about. It's like pronoun use - he, she, it - one assumes people can figure out the referent. This stuff is very hard for computers to understand and get right, but Cyc does both.

"If computers were human," Lenat told us, "they'd present themselves as autistic, schizophrenic, or otherwise brittle. It would be unwise or dangerous for that person to take care of children and cook meals, but it's on the horizon for home robots. That's like saying, 'We have an important job to do, but we're going to hire dogs and cats to do it.'"

Cyc has been in development since 1984 and its knowledge base currently contains over one million human-defined assertions, rules or common sense ideas. Yet it's still barely found practical use. I'm certainly not planning on reproducing that level of effort.

I think we're back to virtualizing the cat ...