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!

---