The aim of this post is to describe a fully automatic proof-finding algorithm that is capable of finding proofs that are sufficiently routine. We hope that if you understand how it works, you will become familiar with many of the concepts and definitions that we will be working with when we design more advanced algorithms.
A mathematics problem can be thought of as a statement that needs proving. Typically that statement involves some assumptions and a conclusion. For instance, the statement "A union of two closed sets is closed", when expressed more formally, gives us two sets $A$ and $B$ in a metric space, and we want to prove that $A\cup B$ is closed given the assumption that $A$ and $B$ are both closed.
However, our proof will typically involve more than mere logical operations: in order to prove that $A\cup B$ is closed, we will use not just the assumptions that we are explicitly given, but also a bank of background knowledge such as the definition of a closed set, the definition of an open set, and the fact that if $\epsilon_1$ and $\epsilon_2$ are positive real numbers then $\min\{\epsilon_1,\epsilon_2\}$ is another positive real number that is less than or equal to both $\epsilon_1$ and $\epsilon_2$.
We therefore think of the algorithm as follows. The input consists of an initial problem state $S_0$, which is a suitably formal statement of what is to be proved, and a library, which is a bank of facts that can be assumed. The algorithm then produces a sequence of problem states $S_0,S_1,\dots,S_k$, each of which is a statement to be proved. This sequence must obey the rule that $S_{i+1}$ implies $S_i$ for each $i$: that is, if we can successfully prove the statement $S_{i+1}$, then that means we have proved the statement $S_i$. If $S_k$ is the trivial statement TRUE, then the algorithm has succeeded, and given us a proof of $S_0$.
In order to transform one problem statement into another, the algorithm has access to a collection of move types, which can be thought of as partial functions (or more generally, since a move type can sometimes be applied in more than one way, relations) defined on the set of all problem states. Thus, if we want to look at things in a very abstract way, we can think of the problem we wish to solve as that of finding a path in a directed graph. The vertices of the graph are all problem states, there is an edge from $S$ to $S'$ if and only if there is a move type $M$ such that $S\to_M S'$ (where this means that $S$ can be transformed to $S'$ using a move of move type $M$), and our aim is to find a directed path from an initial vertex $S_0$ to the vertex TRUE. However, while in full generality the question of how to find a shortest path in a graph is well understood, for this problem the graph has a lot of structure, coming from the interesting way that the vertices and edges are labelled. We thus face the problem of understanding how these labellings can enable us to find short paths much more quickly, and that is a much more challenging question.
There are a few choices that need to be made, which we briefly comment on here. For example, the above statement contains type declarations such as that $(X,d)$ is a metric space. An alternative might be to quantify over all sets $X$ (which of course form a proper class rather than a set) and all functions $d:X\times X\to\mathbb R$ and then to adopt the statement $\text{metric_space}(X,d)$ as an assumption. Or we might prefer to fix once and for all a metric space $X$ instead of universally quantifying over them, to reflect the way a human mathematician would state the theorem starting with the words "Let $(X,d)$ be a metric space." Also, $\text{is_closed}$ is treated here as a two-variable predicate (corresponding to the idea of one set being closed in another) rather than a one-variable predicate with $X$ being considered to be clear from the context. But these are more like implementation details than fundamental aspects of the algorithm.
It is often convenient to represent a problem state by simply listing the type declarations, the assumptions, and the desired conclusion. For example, the above formula can be represented in the following way. $$\begin{array}{|c|} \hline (X,d): \text{metric space}\\ A: \text{subset of }X\\ B: \text{subset of }X\\ \hline \\ \hline \text{is_closed}(A,X)\\ \text{is_closed}(B,X)\\ \hline \\ \hline \text{is_closed}(A\cup B,X)\\ \hline \end{array}$$ We call this kind of representation a tableau. We call the assumptions hypotheses and the statement or statements to be proved targets. It is important that tableaux and logical formulae should be interchangeable -- that is, a tableau should just be a convenient alternative notation for a formula, and we should have a simple algorithm that can convert formulae into tableaux and tableaux into formulae. This is straightforward for examples such as the one above, but can become more complicated for formulae that involve several connectives and/or alternations of universal and existential quantifiers. We have not yet developed a tableau notation that is sufficiently powerful to express all formulae, but we can deal with most of the formulae that arise in practice. One important point is that the hypotheses are implicitly linked by "and" and so are the targets.
In this section, we give a list of basic move types (there are also some more advanced ones, but we shall not discuss them in this introductory post), followed by a brief explanation of each one. In the next section, as a way of demonstrating how the move types work in practice, we shall discuss how they can be used to solve the problem about closed sets.
This is the process of taking a high-level statement such as "$f$ is continuous" and using a definition (which will be stored in the library) to convert it into a lower-level statement such as $$\forall\epsilon > 0\ \forall x\in X\ \exists\delta > 0\ \forall y\in X\ d(x,y) < \delta \implies d(f(x),f(y)) < \epsilon.$$ It comes in various flavours. For example, it can also be used to convert the statement $x\in f^{-1}(A)$ into the statement $f(x)\in A$ or to convert a term $\tan\theta$ into a term $\sin\theta/\cos\theta$, or a term $e^x$ into a term $\sum_{n=0}^\infty x^n/n!$.
If we have a hypothesis $\forall u\ P(u)\implies Q(u)$ and another hypothesis $P(x)$, this allows us to add a hypothesis $Q(x)$. More generally, if we have a hypothesis $\forall u\ P_1(u)\ \wedge\ \dots\ \wedge\ P_k(u)\implies Q(u)$ and for each $i$ we have the hypothesis $P_i(x)$, then again it allows us to add the hypothesis $Q(x)$.
Modus ponens is usually presented as the deduction of $Q$ from the statements $P$ and $P\implies Q$. However, in practice it is almost always used in the above quantified form, to the point where "bare" modus ponens can be quite confusing.
Logically this is the same as modus ponens, at least if we regard the results in the library as a huge collection of additional hypotheses that we are free to use, but in practice it feels quite different. Basically it's modus ponens as above, but where the result $\forall u\ P(u)\implies Q(u)$ is in the library rather than being stated as a hypothesis. For example, suppose that a human mathematician wishes to prove that a function $f:[0,1]\to\mathbb R$ is bounded and is given the information that $f$ is differentiable. They would feel free to argue first that $f$ must be continuous (using the library result $\forall g:\mathbb R\to\mathbb R\ \text{is_differentiable}(g)\implies\text{is_continuous}(g)$) and then, having observed that $[0,1]$ is a closed bounded interval, that $f$ must be bounded (using the library result that if $X\subset\mathbb R$ is a closed bounded interval and $g:X\to\mathbb R$ is continuous, then $g$ is bounded).
Also known as backwards reasoning, this is the process of replacing a target $Q(x)$ by the target $P(x)$ given the hypothesis $\forall u\ P(u)\implies Q(u)$. In a human write-up, one might say, "We would like to prove $Q(x)$. Since for every $u$, $P(u)\implies Q(u)$, it is sufficient to prove $P(x)$." Again, there is a "bare" form of modus tollens that rarely makes an appearance in a typical mathematical proof, though it is formally correct.
This is to the previous move type as move type 3 was to move type 2. That is, the statement $\forall u\ P(u)\implies Q(u)$ belongs to the library instead of being stated as a hypothesis.
Suppose our target statement is of the form $\exists u\ P(u)$ and we have some information about a variable or more complex term $x$ of the same type as $u$. Then we can replace the target by $P(x)$. (For those unfamiliar with the notion of type, you can think of it as simply being the kind of mathematical object you are talking about -- a metric space, an element of a given vector space, etc. If we want to prove that there exists an object $u$ of a certain kind that satisfies a property $P$ that applies to objects of that kind, then we will need to choose as $u$ an object of the same kind.) Similarly, if we have a hypothesis of the form $\forall u\ P(u)$ (where $P(u)$ might be of the form $Q(u)\implies R(u)$), and if we have an object $x$ of the same type as $u$, then we are free to replace the hypothesis by $P(x)$.
Note that from the point of view of writing down a correct proof, the requirement that $x$ should be "already present" in the problem state is unnecessary: if we can somehow define a term $x$ of the right type, and if it does the job we want of it, then the proof is valid. However, this would not be a move type in the sense we are talking about here, since it is too open ended: we do not have a simple algorithm that will obey the command "Instantiate this variable in such a way that it will lead us to the problem state TRUE." Choosing how to instantiate variables in non-trivial ways is a major part of the challenge of solving mathematical problems, so it is a complex step that needs to be achieved only after a sequence of more basic move types has been used.
If we cannot immediately see how to instantiate a variable, an extremely useful technique is simply to behave as if it is chosen and to continue with other move types. Often the result is to convert the problem state into one for which the choice of variable becomes much more obvious. This technique is strongly analogous to what we do when solving a quadratic equation: we do not immediately try to choose a value for the variable, but instead apply techniques such as completing the square, with the result that the solutions eventually become obvious.
How should we regard this as a logical operation? One way of thinking about it is as an application of the rule that the statement $P\implies\exists x\ Q(x)$ is equivalent to the statement $\exists x\ P\implies Q(x)$. So we start with the problem state $P\implies\exists x\ Q(x)$, and transform it into the problem state $\exists x\ P\implies Q(x)$ in order to allow ourselves to apply moves inside scope of the quantifier that would otherwise be blocked. This will become clearer with an example or two.
A similar operation is sometimes useful with universally quantified hypotheses. We might be confident that we want to apply such a hypothesis but without quite being sure what we should apply it to. Again, it may help just to "pretend we have chosen it", apply some deductions and logical manipulations in order to simplify the requirements it should satisfy, and then choose it. We can regard the initial creation of a metavariable as replacing the statement $(\forall x\ P(x))\implies Q$ by the statement $\exists x\ (P(x)\implies Q)$. It is slightly counterintuitive that these two statements are equivalent, but they are (at least if there exists $x$ such that $P(x)$).
If one has a target statement of the form $\forall x: \text{type T}\ Q(x)$, a first step is very often to write "Let $x$ be of type T" and to proceed to prove the statement $Q(x)$. That is, the focus switches from proving $Q(x)$ for all $x$ to proving one for a single arbitrary $x$. We can think of this as converting the statement $P\implies\forall x\ Q(x)$ into the equivalent statement $\forall x\ P\implies Q(x)$. On the other side, if we have a hypothesis of the form $\exists x\ P(x)$, we often write "Let $x$ be such that $P(x)$" and from that moment on we regard $x$ as fixed (but as something we know nothing about other than that it satisfies $P$). We can regard that as replacing $(\exists x\ P(x))\implies Q$ by $\forall x\ (P(x)\implies Q)$.
A few examples of these are as follows.
There are two things left to explain. One is how a suitable sequence drawn from the above move types can be used to solve a simple problem. The other is to describe an algorithm that will select the right sequence of move types with (in this particular case, and for many other routine problems) no backtracking. In this section we concentrate on the first point.
Our initial problem state, in tableau form, is the following. $$\begin{array}{|c|} \hline (X,d): \text{metric space}\\ A: \text{subset of }X\\ B: \text{subset of }X\\ \hline \\ \hline \text{is_closed}(A,X)\\ \text{is_closed}(B,X)\\ \hline \\ \hline \text{is_closed}(A\cup B,X)\\ \hline \end{array}$$
From this point on, we shall omit the type declarations for $X$, $A$ and $B$, though they should be thought of as present behind the scenes. Our first move type will be an expansion, which we apply to the predicate "is_closed" in the target. Already an important issue arises, which is that there are at least three expansions one might imagine using. One is that a set is closed if and only if its complement is open. Another bypasses that "intermediate" expansion and goes for a set $F$ being closed if and only if for every point not in the set there is a ball containing that point that is disjoint from the set. And a third is that a set is closed if and only if it is closed under taking limits of sequences. Any one of these choices leads to a sensible proof, so we will probably want most programs we write either to have a small degree of interactivity, to allow the user to choose when there is more than one sensible option, or to present several sensible proofs when they exist. (For the latter, one has to be careful if there are several choice points, as the number of proofs could then explode.) For this presentation let us go for the second of these expansions. $$\begin{array}{|c|} \hline \text{is_closed}(A,X)\\ \text{is_closed}(B,X)\\ \hline \\ \hline \forall x\in X\ x\notin A\cup B\implies\exists\delta > 0\ B_\delta(x)\cap(A\cup B)=\emptyset\\ \hline \end{array}$$
Next, we peel the universal quantifier over $x$. In tableau form we can represent this peeling as follows. $$\begin{array}{|c|} \hline x: \text{element of }X\\ \hline \\ \hline \text{is_closed}(A,X)\\ \text{is_closed}(B,X)\\ \hline \\ \hline x\notin A\cup B\implies\exists\delta > 0\ B_\delta(x)\cap(A\cup B)=\emptyset\\ \hline \end{array}$$
Applying the rule that allows us to replace $P\implies(Q\implies R)$ by $(P\ \wedge\ Q)\implies R$, we can transform this to $$\begin{array}{|c|} \hline \text{is_closed}(A,X)\\ \text{is_closed}(B,X)\\ x\notin A\cup B\\ \hline \\ \hline \exists\delta > 0\ B_\delta(x)\cap(A\cup B)=\emptyset\\ \hline \end{array}$$ Again we have silently removed the type declaration.
A very basic expansion allows us to replace $u\notin U$ by $\neg(u\in U)$, so we do that. $$\begin{array}{|c|} \hline \text{is_closed}(A,X)\\ \text{is_closed}(B,X)\\ \neg(x\in A\cup B)\\ \hline \\ \hline \exists\delta > 0\ B_\delta(x)\cap(A\cup B)=\emptyset\\ \hline \end{array}$$
Expanding the definition of union, we obtain the following. $$\begin{array}{|c|} \hline \text{is_closed}(A,X)\\ \text{is_closed}(B,X)\\ \neg(x\in A\ \vee x\in B)\\ \hline \\ \hline \exists\delta > 0\ B_\delta(x)\cap(A\cup B)=\emptyset\\ \hline \end{array}$$
Applying de Morgan's law and also splitting up the resulting conjunction into two separate hypotheses (see the second example of move type 9) gives the following (after two moves, but we shall jump straight to the result). $$\begin{array}{|c|} \hline \text{is_closed}(A,X)\\ \text{is_closed}(B,X)\\ \neg(x\in A)\\ \neg(x\in B)\\ \hline \\ \hline \exists\delta > 0\ B_\delta(x)\cap(A\cup B)=\emptyset\\ \hline \end{array}$$
Next, we expand the two further instances of "is_closed", and then the two instances of "$\notin$" that result. (So again, the tableau shown is the result of several moves and not just one.) $$\begin{array}{|c|} \hline \forall u\in X\ \neg(u\in A)\implies\exists\alpha > 0\ B_\alpha(u)\cap A=\emptyset\\ \forall v\in X\ \neg(v\in B)\implies\exists\beta > 0\ B_\beta(v)\cap B=\emptyset\\ \neg(x\in A)\\ \neg(x\in B)\\ \hline \\ \hline \exists\delta > 0\ B_\delta(x)\cap(A\cup B)=\emptyset\\ \hline \end{array}$$
There are now two opportunities to apply modus ponens using hypotheses, so we do both of them. For tidiness of presentation we remove the hypotheses that were used and will not be used again. $$\begin{array}{|c|} \hline \exists\alpha > 0\ B_\alpha(x)\cap A=\emptyset\\ \exists\beta > 0\ B_\beta(x)\cap B=\emptyset\\ \hline \\ \hline \exists\delta > 0\ B_\delta(x)\cap(A\cup B)=\emptyset\\ \hline \end{array}$$
Next, we peel the existential quantifiers over $\alpha$ and $\beta$. $$\begin{array}{|c|} \hline \alpha: \text{positive real number}\\ \beta: \text{positive real number}\\ \hline \\ \hline B_\alpha(x)\cap A=\emptyset\\ B_\beta(x)\cap B=\emptyset\\ \hline \\ \hline \exists\delta > 0\ B_\delta(x)\cap(A\cup B)=\emptyset\\ \hline \end{array}$$ There is a small issue here about whether the type of $\alpha$ should be "positive real number" or whether it should be "real number" with the positivity being a hypothesis. For many $\epsilon$-$\delta$ arguments, the first option seems a better reflection of how we think of these numbers.
Because we don't know what $\delta$ is, we're not in a good position to deduce the target statement, so this is a good time to turn $\delta$ into a metavariable. In the notation we are using here, we shall indicate this by removing the existential quantifier and attaching a bullet to $\delta$. (For more complicated problems, it becomes important to specify carefully which bulleted variables are allowed to depend on which other variables. The main thing here is that $\delta$ can, and indeed will, depend on $\alpha$ and $\beta$.) $$\begin{array}{|c|} \hline \\ \hline B_\alpha(x)\cap A=\emptyset\\ B_\beta(x)\cap B=\emptyset\\ \hline \\ \hline B_{\delta^\bullet}(x)\cap(A\cup B)=\emptyset\\ \hline \end{array}$$ Once again, we have removed the type declarations.
Now let us expand the target. There is some choice about how to do this, but the following one will turn out to be convenient. $$\begin{array}{|c|} \hline \\ \hline B_\alpha(x)\cap A=\emptyset\\ B_\beta(x)\cap B=\emptyset\\ \hline \\ \hline \forall y\in X\ y\in B_{\delta^\bullet}(x)\implies y\notin A\cup B\\ \hline \end{array}$$
Next, we peel the universal quantifier and also turn the premise of the target implication into a hypothesis. $$\begin{array}{|c|} \hline y: \text{element of }X\\ \hline \\ \hline B_\alpha(x)\cap A=\emptyset\\ B_\beta(x)\cap B=\emptyset\\ y\in B_{\delta^\bullet}(x)\\ \hline \\ \hline y\notin A\cup B\\ \hline \end{array}$$
Now let us do some basic propositional calculus and expansion to reformulate the target. $$\begin{array}{|c|} \hline \\ \hline B_\alpha(x)\cap A=\emptyset\\ B_\beta(x)\cap B=\emptyset\\ y\in B_{\delta^\bullet}(x)\\ \hline \\ \hline \neg(y\in A)\\ \neg(y\in B)\\ \hline \end{array}$$
Next, we expand the first two hypotheses. $$\begin{array}{|c|} \hline \\ \hline \forall u\in X\ u\in B_\alpha(x)\implies u\notin A\\ \forall v\in X\ v\in B_\beta(x)\implies v\notin B\\ y\in B_{\delta^\bullet}(x)\\ \hline \\ \hline \neg(y\in A)\\ \neg(y\in B)\\ \hline \end{array}$$
Since we've been getting rid of $\notin$, we continue the process. (Alternatively we could reinstate it in the target statements.) $$\begin{array}{|c|} \hline \\ \hline \forall u\in X\ u\in B_\alpha(x)\implies\neg(u\in A)\\ \forall v\in X\ v\in B_\beta(x)\implies\neg(v\in B)\\ y\in B_{\delta^\bullet}(x)\\ \hline \\ \hline \neg(y\in A)\\ \neg(y\in B)\\ \hline \end{array}$$
We can now do (straightforward, non-library) modus tollens twice, to change our target statements. For tidiness, we get rid of the statements that have been used in the process. $$\begin{array}{|c|} \hline \\ \hline y\in B_{\delta^\bullet}(x)\\ \hline \\ \hline y\in B_\alpha(x)\\ y\in B_\beta(x)\\ \hline \end{array}$$
At this stage, maybe the library contains a result about open balls that says that if $\theta_1\leq\theta_2$ then $B_{\theta_1}(x)\subset B_{\theta_2}(x)$. But let's not assume that that's the case, and instead expand statements of the form $u\in B_\theta(v)$ as $d(u,v)<\theta$. $$\begin{array}{|c|} \hline \\ \hline d(y,x) < \delta^\bullet\\ \hline \\ \hline d(y,x) < \alpha\\ d(y,x) < \beta\\ \hline \end{array}$$
Now comes a slightly complicated version of "library modus tollens". A human mathematician will look at the assumption $d(y,x) < \delta^\bullet$ and see easily that in order to be able to deduce that $d(y,x) < \alpha$ it will be sufficient if $\delta^\bullet\leq\alpha$. This isn't modus tollens, but if the library contains the result $$\forall a,b,c\in\mathbb R\ a < b\ \wedge\ b\leq c\implies a < c$$ then we find that we can instantiate it with $a=d(y,x)$, $b=\delta^\bullet$ and $c=\alpha$. That would give us exactly what we want, were it not for the fact that we are missing the hypothesis $\delta^\bullet\leq\alpha$. But modus tollens (in a version with multiple hypotheses) allows us to replace the target by the missing hypothesis. Applying this move twice, and removing the used up statements, we obtain the following problem state. $$\begin{array}{|c|} \hline \\ \hline \hline \\ \hline \delta^\bullet \leq \alpha\\ \delta^\bullet \leq \beta\\ \hline \end{array}$$
At this point, either one can try to solve the problem of finding a positive real number that is bounded above by two given positive real numbers (one approach is to try $\alpha$ and observe that the only way it can fail is if $\beta < \alpha$, in which case $\beta$ works), or one can just assume that there is an appropriate library result that tells us that $\min\{\alpha,\beta\}$ does the job. Since we have illustrated almost all the move types, we shall opt for the latter assumption and declare the problem solved at this point. (More precisely, we can use the library result to reduce the target statement, and hence the entire problem state, to TRUE.)
There are many potential ways of doing this, so the aim here is not to say how it should be done, but to give an idea of how it can be done in such a way as to solve problems that are sufficiently routine.
A first comment is that there are certain "tidying" moves that are almost always worth doing without even thinking. The main examples are peeling and the move that takes a target of the form $P\implies Q$ and turns $P$ into a hypothesis and leaves $Q$ as the target. Another example is taking a hypothesis or target of the form $P\ \wedge\ Q$ and splitting it up into two hypotheses or targets $P$ and $Q$. So at least for a basic algorithm one can just get it to do those moves whenever they are possible.
"Reasoning" moves such as modus ponens and modus tollens are nearly always a good idea if the problem is fairly routine and the library is not involved, so they can be of high priority, but less high than tidying moves. If library statements are involved, then the quality of a reasoning move depends to some extent on how well the library result fits the problem state. If, for example, there is a target $Q(x)$ and a library result of the form $\forall y\ P_1(y)\ \wedge\ P_2(y)\implies Q(y)$, then that will not be very appealing if neither $P_1(x)$ nor $P_2(x)$ is a hypothesis, as that would replace the target with two new targets. But if one of $P_1(x)$ and $P_2(x)$ is present (as was the case near the end of the proof given above), then it becomes a significantly better move.
Instantiation of a quantified variable with a term of the same type that is already present is again quite a good move for routine problems, though for more complicated problems it is better to have some evidence that the instantiation will be fruitful. (Such evidence might be that the variable is required to satisfy a condition and the term satisfies that condition, or perhaps has a different property that gives one reason to hope that it might satisfy the condition.)
It is nice to reason at a high level when that is possible, so expanding definitions is something of a last resort: when all else fails we try to prove the statement in a more complicated lower-level way. This applies more to expanding predicates. A more basic expansion such as replacing $x\in f^{-1}(A)$ by $f(x)\in A$ or $x\in A\cap B$ by $x\in A\ \wedge\ x\in B$ (a sign that these expansions are more basic is that they don't introduce quantifiers) has more of the flavour of a tidying move, so tends to have higher priority.
Creating a metavariable is something one tends to do when one needs to instantiate a quantified variable and there does not appear to be a variable or term that will do the job. If one is going to have to generate a new variable or build some more complex term, then very often one will want to manipulate the problem state quite a bit more before doing so, and that is where metavariables come into their own. This again has fairly low priority -- one does it when a bit "stuck" -- but low priority certainly doesn't mean that it happens rarely.
The ROBOT algorithm worked by taking principles such as the above ones and simply listing move types in order of priority, repeatedly doing a move with move type of the highest availble priority. (The list of move types was a more refined -- for instance, expanding a target was given higher priority than expanding a hypothesis.) If you look back through the sequence of problem states in the previous section, you will see that the moves chosen at each stage are broadly speaking chosen with the priorities just suggested.
Most of the time, that worked very smoothly, but occasionally small issues would arise such as which expansion to choose when there is more than one option, or what there is available in the library. A lot of the detailed work is in dealing with such issues, ideally not in ad hoc ways but in coming up with more sophisticated principles (that is, not just putting move types in order but also taking into account features of the problem state) that will deal with them in satisfactorily general ways. Some examples of such principles will be given in future posts.