Automated Reasoning and Symbolic AI

In the early twentieth century, logicians developed algorithms to decide the truth of mathematical statements in restricted domains. For example, Mojżesz Presburger proved in 1926 that there is an algorithm to decide the truth of any first-order statement about the integers as an ordered abelian group, and Alfred Tarski proved in 1933 that there is a similar algorithm for the real numbers as an ordered field. The first class of statements is now known as Presburger Arithmetic or Linear Integer Arithmetic, and the second is known as the Theory of Real Closed Fields or, to computer scientists, Nonlinear Real Arithmetic. The algorithms are examples of decision procedures.

In 1936, Alan Turing published his definition of computability and showed that there is, however, no decision procedure for the integers with addition and multiplication. The result is implicit in Kurt Gödel’s 1931 paper on incompleteness. However, early logicians knew that one could do the next best thing, namely, systematically search for proofs in a suitable axiomatic system.

Almost as soon as digital computers were available, researchers began implementing search procedures and decision procedures, and these are now an important part of computer science and symbolic AI. Here, we explore some applications to mathematics.

SAT solvers

A formula in propositional logic is true or false depending on the truth assignments to the variables. A formula is said to be satisfiable if there is some truth assignment that renders it true. There is an easy algorithm to decide whether a propositional formula is satisfiable: write out the truth table and check whether any line evaluates to true. Propositional satisfiability is a paradigmatic NP-complete problem, so we do not expect an efficient algorithm. Surprisingly, however, modern satisfiability solvers, or SAT solvers for short, work extremely well on problems that come up in practice. They can decide the satisfiability of industrial formulas with tens of millions of variables, often in minutes. An annual SAT competition evaluates the state of the art.

Since many combinatorial problems can be encoded as a propositional formula, this provides a recipe for proving mathematical theorems,

• The Pythagorean triples problem
• Schur numbers
• Keller’s conjecture
• The happy ending problem

In 2021, Giles Gardam used a SAT solver to refute the first of Kaplansky’s conjectures. We recommend this talk on the result.

Bernardo Subercaseaux’s SAT for Mathematics page lists several interesting applications of SAT solvers to mathematics.

First- and higher-order provers

First-order logic is expressive enough to write down the axioms of Zermelo-Fraenkel set theory, a powerful foundation for mathematics. However, even provability in pure first-order logic, with no axioms at all, is undecidable. First-order provers, therefore, have to resort to proof search and the realm of Automated Theorem Proving (ATP). The TPTP library (Thousands of Problems for Theorem Provers) contains benchmarks for automated provers, and the annual CADE ATP System Competition (CASC) evaluates the state of the art. Many ATP systems today go beyond first-order logic, including aspects of higher-order reasoning and/or arithmetic.

In 1996, William McCune’s automated theorem prover, EQP, made the New York Times for proving the Robbins conjecture. A dual class of tools, model finders, can sometimes find a counterexample to a first-order entailment, showing that there is a model where the hypotheses hold but the conclusion does not. First-order provers and model finders have been used to study algebraic structures like quasigroups and loops.

ATP is also used to support formalization. Many proof assistants have built-in procedures for proof search. With sledgehammer technology, of which Isabelle’s is the best example, a proof assistant calls an external prover and, if the latter is successful, tries to reconstruct the proof internally.

Both first-order provers and model-finders were used in the Equational Theories Project, led by Terence Tao. The project highlighted both the capabilities of automated reasoning technology and the use of the Lean proof assistant, social media, and other technology to support large-scale collaboration.

Decision procedures and SMT solvers

Many proof assistants implement decision procedures for integer and real arithmetic, as well as domain-specific procedures for reasoning about commutative rings and fields. A class of automated reasoning tools known as Satisfiability Modulo Theories (SMT) solvers combine general first-order reasoning with domain-specific theorem provers. In computer science and industry, they are commonly used for hardware and software verification. The Satisfiability Modulo Theories library provides benchmarks, and a corresponding competition assesses the state of the art.

They are also used in sledgehammers, thereby supporting the formalization of mathematics. Lean’s powerful grind procedure uses SMT techniques.