A more impressive system is Siemion Fajtlowicz’s
Graffiti (Fajtlowicz 1988), which generates conjectures in graph theory. More recently, Craig Larson
extended Fajtlowicz’s Graffiti into a more general
framework for mathematical conjecture making in
discrete math (Larson and Cleemput 2016; 2017). For
an early survey on these systems, see Larson (2005).
However, these examples all focus on a general
theory like propositional logic, number theory, or
graph theory. For AI applications, more often we
want to prove theorems in a very specific theory for
some very specific purpose. For instance, we could be
given a planning domain such as the logistics
domain, and we want to know if there are special
properties about the domain that can help prune the
search space for the planner in hand. Finding these
properties is the same as discovering theorems, once
the domain is axiomatized by a formal theory, for
example, in the situation calculus. As another example, in software verification, we may want to prove
that a certain postcondition holds when the input
satisfies a certain precondition. This relationship can
be naturally formulated as a theorem-proving problem and is, in general, intractable. It helps, then, to
discover some useful properties about the program in
question to make the theorem-proving task easier. In
fact, much of the formal work on verifying sequential
programs can be said to be about discovering suitable
loop invariants as pioneered in Hoare’s logic (Hoare
In the past, my colleagues and I have developed
programs for discovering state invariants in planning
(Lin 2004), for discovering theorems that capture
strong equivalence in logic programming (Lin and
Chen 2007), for identifying conditions that capture
the uniqueness of pure Nash equilibria in games in
normal form (Tang and Lin 2011a), and for checking
the consistency of social choice axioms by translating them to SAT (Tang and Lin 2009). Our work has
inspired others to apply similar approaches to other
problems (for example, Geist and Endriss 2011; Brandl et al. 2015; Brandt and Geist 2016; Brandl, Brandt,
and Geist 2016). For instance, instead of SAT, Brandl,
Brandt, and Geist (2016) used SMT in their work on
showing the incompatibility of certain notions of
efficiency and strategy-proofness.
In this article, I will outline a general approach to
machine theorem discovery. I will review some of our
earlier work and recast it in a general framework. As
it will become clear, the key is to formulate hypotheses in a formal logical language.
In a nutshell, theorem discovery can be viewed as an
iterative two-step process:
while (true) do
1. Find a reasonable conjecture;
2. Verify the conjecture.
Figure 1. An Algorithm for Machine Theorem Discovery.
1 Language description: sorts, predicates, constants, functions.
2 A collection of sets of objects to construct models of the language.
3 A model con;rmation relation between models M and sentences ϕ:
M con;rms ϕ if M satis;es the required property about ϕ, provided
that M is a model of the domain theory.
4 (Optional) A theorem prover for checking if a sentence is a theorem
in the given theory.
5 A speci;cation of the space of hypotheses: by defaults, all atomic
sentences, binary clauses, type information (unary predicates),
functional dependencies will be in the space. The user can also
Output: Weakest conjectures.