There are mechanised approaches to algebra, combinatorics, numerical analysis, etc , but this book is not about those subjects, it is about logic: all we can discuss in this section is the choreography of ", $, Ù, Ú and Þ , and reinforce the importance of the scope of variables and hypotheses. We cannot do the creative part of mathematics, because the solution to a problem in number theory, for example, may be ``simply'' an ingenious observation about z(s) = ån = 1¥ n-s or counting points in a cube in Rn.
The steps which can be automated are the obvious ones, in a technical sense: this literally means ``in the way'' in Latin. It is obvious how to go through a foreign airport, not because you know it intimately, but because there are signs telling you where to turn whenever you need them (you hope). This is also known as exam technique: write down and exploit what you already know. Whereas the box or sequent rules of predicate calculus from the previous section are the laws of the game of proof, the heuristics are hints on the tactics. This section is based on teaching first year informatics students to construct proofs on paper. Of course this will also give some idea of how to write a program to do it, but the strategy for making choices when backtracking is needed raises issues far outside the scope of this book [Pau92].
George Polya [Pol45] and Imre Lakatos [ Lak63] gave two classic accounts of heuristics in mathematics, using Euclidean geometry for examples. Polya's advice - make a plan and carry it out, compare your problem with known theorems, etc - is extremely valuable to help students of mathematics (and professionals) get past the blank sheet of paper, but treats more strategic aspects of proof than we can. An early theorem prover was based on his methods of drawing diagrams and formulating conjectures and counterexamples; that this seems odd now shows both the sophistication of modern proof theory and perhaps also the danger of isolation from the traditional instincts of mathematicians.
Nikolas de Bruijn's AUTOMATH project (late 1960s) set out to codify existing mathematical arguments, rather than to find new theorems, and this remains the research objective of automated reasoning. Johan van Benthem Jutting (1977) translated Edmund Landau's book Foundations of Analysis into AUTOMATH and analysed the ratio by which the text is magnified, which was approximately constant from beginning to end. Similar work has been done for other areas of mathematics.
There are certain dangers inherent in the formalisation of mathematics. Systems of axioms acquire a certain sanctity with age, and in the how of churning out theorems we forget why we were studying these conditions in the first place. Computer languages suffer far more from this problem: nobody would claim any intrinsic merit for FORTRAN or HTML, but sheer weight of existing code keeps them in use. Through the need for a standard - any standard - a similar disaster could befall mathematics if set theory were chosen. As with any programming, and also with the verification of programs, far more detail is required than is customary in mathematics. G. H. Hardy (1940) claimed that there is no permanent place in the world for ugly mathematics, but I have never seen a program which is not ugly. Even when the mathematical context and formal language are clear, we should not perpetuate old proofs but instead look for new and more perspicuous ones.
Theoretical basis By Gentzen's cut-elimination theorem, supposing that G\vdash q is provable, we need only look for a cut-free proof. We can say something about the final lines of such a proof (in sequent calculus) from the structure of the rules other than cut, and in particular the sub-formula property (Remark 1.4.9).
Although we must read a finished proof from top to bottom, the search for and creation of the proof are not so direct. (The commonest misconception about mathematicians amongst the general population is that we act like robots when trying to solve problems.) By the nature of cut- elimination, the heuristics are in fact goal-driven: they proceed mainly in the opposite direction from the reading of the completed proof.
For certain fragments of logic, if there is any proof of G\vdash q then there is one obtainable by means of the following heuristics. Conversely, if we fail, by completeness (Remark 1.6.13) there is a counterexample, which can be obtained from the trace of our proof- attempts.
FACT 1.7.1 Hereditary Harrop formulae are the definite formulae g and goals q respectively defined by the grammar
omitted eqnarray* environment
where a is atomic. If G is a list of definite formulae and q is a goal formula for which G\vdash q is provable, then it has a uniform proof, ie one in which each sequent D\vdash f with f non-atomic is deduced only by means of the introduction rule for the outermost connective of f [MNPS91]. 
So we construct the proof in reverse by dismantling the goal formula.
Resolution When the goal is an atomic formula, logical manipulation has nothing to say, and we have to make use of the database, ie the axioms G given in the problem. These are written at the top of the page, numbering the lines from 1 and giving the justification for each line as `` data.'' The desired conclusion(s) or goals q are written at the bottom, numbering the lines backwards from 99 and giving no reason (yet). We shall progressively add more lines 2, 3, ... and 98, 97, ... and also fill in reasons; the lines which have no reason so far are called pending goals.
REMARK 1.7.2 If the atomic formula q is a goal and the axiom
REMARK 1.7.3 The program is non-deterministic, because there may be several procedures for q: if using one of them fails to find a proof, we backtrack and try another. To do this by hand, place a new sheet of tracing paper over the proof so far each time you have to make a choice; then if the choice is wrong you can discard the working which depended on it and return to the immediately preceding state. Only the last choice is discarded: earlier ones may still be viable until all possibilities at this stage have been exhausted. This means that the choices in the search form a nested system in the heuristics, but this is independent of the nested contexts (boxes) in the completed proof.
REMARK 1.7.4 Similarly, a predicate in the database of the form
Suppose that we want to use this Horn clause to prove (solve the query) q[[(a)\vec],[(b)\vec]]. By ("E ) we put [(a)\vec] for [(x)\vec], and by (Þ E ) we have to prove f[[(b)\vec],[(d)\vec],[(e)\vec]] and match [(a)\vec] = [(c)\vec], substituting suitable terms [(d)\vec] and [(e)\vec] for [(y)\vec] and [(z)\vec].
EXAMPLE 1.7.5 A database application might have axioms such as
journey[x,z,u+v] Ü journey[x,y,u], journey[y,z,v] .
train[London, Bristol, £ 40] train[London, York, £ 40] train[London, Paris, £ 100] train[Paris, Nice, £ 80] train[x,y,u] train[y,x,u] journey [x,y,u] train[x,y,u]
Then for the query journey[Nice, Bristol, u] we expect not only a proof that one can go from Nice to Bristol by rail, but also the route and cost. So when we assert $x.q[x] we give a definite answer as to what x is - these substitutions are the result of the computation.
REMARK 1.7.6 John Robinson showed how to do this by resolution (1965). Gentzen's Hauptsatz cannot eliminate cuts when axioms are used, and resolution deals with those that remain. It involves substitution of terms for variables, but each resolution step only gives partial information about what has to be substituted: the constraints which fully determine the value may come from quite different parts of the proof (execution of the program).
We can use declarations (Definition 1.6.8) to record this information:
= .2 - omitted proofbox environment
omitted proofbox environment
Here f[[(b)\vec],[(y)\vec]0] is a new goal, to be satisfied by further resolution, as we have done with q. The partial proof on the right illustrates the similar way in which existential goals are handled.
The equations [(a)\vec] = [(c)\vec] are also new goals. If these terms are simply names for individuals (London, York, etc ) and there are no axioms to say that individuals with different names can be equal then we can see immediately whether or not the equations hold. If not, this attempt at resolution fails and we backtrack to find another one. In practice this is done by database-searching techniques.
The programming language PROLOG does resolution and unification. Despite its name, it does not in fact deal with the logical connectives and quantifiers, but what we shall come to call the algebraic fragment (although this will not look like algebra until Section 4.6). The denotational semantics, based on the work of Jacques Herbrand (1930), will be discussed in Sections 3.7 and 3.9.
Unification Goals involving function-symbols need another technique, called unification. How to do unification is easy: the difficult part is to see what it means. The functions in question are those whose values might be enumerated in a database, such as mother_of, not arithmetic.
REMARK 1.7.7 A goal of the form r([(u)\vec]) = r([(v)\vec]), where r is an operation-symbol for which no laws are known, can only follow by substitution:
This does not mean that every function is injective. We want to carry on building the logical structure of a proof, possibly without knowing what terms serve as the subjects of predicates. We postpone filling in these terms, and then try to do so as non-specifically as possible, using only the building blocks we already have in the term calculus of the object-language. The possibility that two terms might denote the same thing is only considered if the terms themselves were formed in the same way.
The point is that
Eventually, if neither type of failure (clash or occurrence) happens, the system of equations will be saturated, ie none of these rules will expand it further. Then some of the indeterminates will be expressed as terms, possibly involving the others.
REMARK 1.7.8 Some of the indeterminates may be independent, for example y0 is arbitrary in the equation x0 = r(y0). The full solution to the unification problem is not unique, since we may put anything we please for y0. However, the solution in which y0 is left as we have it is the most general unifier in that
We can in fact eliminate the confusion of working backwards from goals, and reduce unification to a kind of algebra. A theory with operation-symbols of various arities (numbers of arguments) but no laws is called a free theory, and unification is the study of its free or term model. We shall take this up formally in Chapter VI and return to unification in Section 6.5 , where we shall see that Remark 1.7.7(g) can be simplified.
Unification in theories with laws is more difficult. It is possible to handle commutativity and associativity, at the cost of uniqueness: there is now a family of maximally general unifiers. Unification under the distributive law would give a uniform way to solve Diophantine equations, but Yuri Matajasivi vc showed that this is undecidable (1970). Gérard Huet showed that unification in higher order l-calculi is also undecidable [ Hue73].
Box-proof heuristics Now we turn to the logical symbols themselves. The following methods belong in a course on the predicate calculus: it is probably better to teach resolution quite separately. Unless we say otherwise, any boxes are drawn as large as possible, extending from the end of the database to the first pending goal.
REMARK 1.7.9 The uniform proof (Fact 1.7.1) is found as follows:
=.3 omitted proofbox environment omitted proofbox environment
-.5 -2em 2 omitted proofbox environment -28.4pt omitted proofbox environment
($x.f [x])Þ q º "x.(f[x] Þ q). Recall, however, that the ($E ) -box is open-ended below (Remark 1.6.5), so as long as the variable x does not occur elsewhere, we can simply add f[x] to the data without a box. It is to our advantage to do this as soon as possible, because there may be many things satisfying f, and it could be relevant later that the same one plays two or more different roles in the argument, although to say that we ``choose'' a witness does not mean that an actual individual is selected (Remark 1.6.7). The original axiom $x.f[x] will not be needed again.
Subject to scoping of variables, these boxes may be nested in any order and so may be taken together in a single step.
Notice that ("Á ) and ($E ) mirror each other, but ($Á ) and ("E ) do not. This is because a goal requires just one proof, whereas a hypothesis may be employed any number of times, or not at all. (Linear logic analyses the reuse of hypotheses, but we shall not consider it in this book.)
REMARK 1.7.10 During resolution, we used declarations ( putx0 = ?) to introduce indeterminates. This was done to allow us to continue building the logical structure of the proof without specifying certain of its details. When we have obtained a valid proof, complete apart from the occurrences of an indeterminate x0, we have to find a term which can be substituted everywhere for it. This term must satisfy any equations in which x0 occurs, irrespective of how they are nested within the proof box, so the unification problem cuts across the scoping structure of the proof. Nevertheless, the term must still be well formed at the point of the declaration: the variables belonging to nested ("Á )- and ($E )-boxes must not be free in it.
REMARK 1.7.11 We have gone beyond Fact 1.7.1 by discussing axioms of the form $x.f[x], fÚy and \lnot f. These are not definite in the sense of Example 1.7.5, because when $x.f[x] is used the program cannot provide an answer for x, and x may remain free in any other answers it gives. Similarly which of f or y holds in fÚy is indeterminate. If the joker (^E) is used to prove $y.q[y], again we have no idea what y is.