Automated reasoning

• 1. Introduction

  ›

  Automated reasoning is the branch of computer science dedicated to understanding how machines can reason, completely or nearly completely, on their own. In 1956, a program called the Logic Theorist did something no machine had done before: it proved thirty-eight of fifty-two theorems drawn from one of the most ambitious books in the history of mathematics. For one of those theorems, the machine found a proof more elegant than the one written by the human authors themselves. That detail plants a question that runs through the entire history of this field: when a machine reasons, is it merely following rules, or is it doing something more?

• 2. Formal Logic as Foundation

  ›

  A formal proof leaves nothing to intuition. Every logical step is supplied without exception, traced back to the fundamental axioms of mathematics. No appeal is made to instinct, even when translating from instinct to logic seems routine. That strictness makes formal proofs less susceptible to error, and it was the development of formal logic that opened the door to automated reasoning as a discipline.

  Principia Mathematica, written by Alfred North Whitehead and Bertrand Russell, stands as a milestone in this tradition. Its aim was to derive mathematical expressions from symbolic logic alone. Published across three volumes in 1910, 1912, and 1913, it built on Russell's earlier 1903 work, The Principles of Mathematics, in which Russell had introduced his famous paradox and argued that mathematics and logic are, at their root, the same thing.

  The question of when automated reasoning truly began is itself contested. Some trace its origin to the Cornell Summer meeting of 1957, which gathered logicians and computer scientists in one room. Others point earlier, to Martin Davis's 1954 implementation of Presburger's decision procedure, a program that proved, formally, that the sum of two even numbers is even. That modest-sounding achievement marked the first time a machine had carried out a logical proof from scratch.

• 3. The Logic Theorist

  ›

  Allen Newell, Cliff Shaw, and Herbert A. Simon built the Logic Theorist in 1956 with a specific aim: to mimic human reasoning. The program was tested against fifty-two theorems from chapter two of Principia Mathematica. It proved thirty-eight of them.

  One result stood apart. For a theorem that Whitehead and Russell had already proved, the Logic Theorist produced a shorter, more efficient derivation, requiring fewer steps than the original. The program's creators tried to publish this finding, but the attempt failed. In 1958, Newell, Shaw, and Simon described the moment in a publication titled The Next Advance in Operation Research, writing that "there are now in the world machines that think, that learn and that create" and that "their ability to do these things is going to increase rapidly."

  That optimism would meet resistance. The field entered what researchers would later call an "AI winter" during the eighties and early nineties, a period of diminished interest and funding. The revival, when it came, was practical rather than philosophical. In 2005, Microsoft began using verification technology across many of its internal projects, and the company was planning to include a logical specification and checking language in its 2012 version of Visual C.

• 4. Proof Systems in Practice

  ›

  The Boyer-Moore Theorem Prover, known as NQTHM, began at Edinburgh, Scotland in 1971. Its design drew on the thinking of John McCarthy and Woody Bledsoe. Built in Pure Lisp, NQTHM worked as a fully automatic theorem prover. Its architecture rested on Lisp as a working logic, a principle of definition for total recursive functions, extensive use of rewriting and symbolic evaluation, and an induction heuristic triggered by the failure of symbolic evaluation.

  HOL Light took a different path. Written in OCaml, it was designed for simplicity: a clean logical foundation, an uncluttered implementation, focused on classical higher order logic.

  Rocq, developed in France and formerly known as Coq, added a capability that set it apart from the others. It can automatically extract executable programs from specifications, producing either Objective CAML or Haskell source code. Properties, programs, and proofs are all written in a single language called the Calculus of Inductive Constructions.

  The table of formal proofs these systems have produced spans decades. In 1986, Shankar used Boyer-Moore to formalize Godel's First Incompleteness theorem. In 2004, Gonthier used Rocq to prove the Four Color theorem. In 2016, Heule and colleagues formalized the Boolean Pythagorean triples problem as a SAT instance, a proof that had no traditional analogue at all.

• 5. Where Reasoning Meets Uncertainty

  ›

  Not all reasoning works from certainty. A significant portion of automated reasoning research addresses problems where the facts are incomplete or contradictory. Non-monotonic reasoning handles situations where conclusions can be retracted when new information arrives. Bayesian inference, fuzzy logic, and reasoning with maximal entropy are among the tools developed for these less-than-certain environments.

  Argumentation sits at the intersection of uncertainty and formal logic. In argumentation systems, constraints of minimality and consistency are applied on top of standard automated deduction. John Pollock's OSCAR system is a specific example: it qualifies as an automated argumentation system, not simply an automated theorem prover, because it handles a richer and more constrained class of reasoning problems.

  Reasoning by analogy, using induction and abduction, also occupies substantial research territory. These methods attempt to extend conclusions beyond what can be strictly proven, drawing on patterns in existing knowledge. The TPTP library, created by Sutcliffe and Suttner in 1998, collects formal logic problems from across these domains and updates regularly. A regular competition at the CADE conference, catalogued by Pelletier, Sutcliffe, and Suttner in 2002, selects problems from TPTP to pit automated theorem provers against one another.

• 6. New Architectures, New Problems

  ›

  In the 2020s, the field found a new context to address. Large language models demonstrated striking abilities but a persistent weakness: they could produce confident, fluent, and wrong answers. Two architectural responses emerged. The first involved reasoning language models designed to spend additional time on a problem before generating an answer. The second involved neuro-symbolic architectures, systems that combine neural networks with symbolic reasoning components to prevent the kind of errors called hallucinations.

  Automated reasoning's application range has grown well beyond theorem proving. Formal logic, mathematics, computer science, logic programming, software verification, hardware verification, and circuit design are all areas where automated reasoning programs are now being applied. The field that once spent a decade proving that the sum of two even numbers is even now contributes to verifying the correctness of chips, software, and, increasingly, the outputs of AI systems themselves.