On Efficiency in Theorem Provers which Fully Expand Proofs into Primitive Inferences

Richard J. Boulton University of Cambridge Computer Laboratory New Museums Site, Pembroke Street Cambridge CB2 3QG, ENGLAND

February 1992

Abstract

Theorem Provers which fully expand proofs into applications of primitive inference rules can be made highly secure, but have been criticized for being orders of magnitude slower than many other theorem provers. We argue that much of this relative inefficiency is due to the way proof procedures are typically written and not all is inherent in the way the systems work. We support this claim by considering a proof procedure for linear arithmetic. We show that straightforward techniques can be used to significantly cut down the computation required. An order of magnitude improvement in the performance is shown by an implementation of these techniques.

1 Introduction

There are many ways to classify mechanical theorem provers. One way is to distinguish between theorem provers that generate proofs entirely in terms of primitive inferences of the logic, and those that do not. We shall refer to these as fullyexpansive and partially-expansive respectively. Let us view a proof produced by a fully-expansive theorem prover as a tree with axioms and preproved theorems as leaf nodes, and applications of primitive inference rules as branch (internal) nodes. A partially-expansive theorem prover may replace certain subtrees of the proof by meta-theorems. Meta-theorems are properties that cannot be expressed directly in the logic, such as “two trees of conjunctions are equivalent if the sets of conjuncts are the same”.

The great advantage of using meta-theoretic properties is that usually far less computation is required to test whether a meta-theorem holds than to construct a full proof using primitive inferences. In our ‘trees of conjunctions’ example, the use of the meta-theorem only requires that the conjuncts be extracted from each of the terms and the two sets be compared for equality. Using primitive inferences the proof has to be constructed (for example) by applications of associative, commutative and various other rules. This is usually far more costly.

The disadvantage of meta-theoretic properties is that they undermine security. When the entire proof is in terms of primitive inferences, the critical code of the theorem prover can be constrained to the procedures which implement the primitive inference rules. These procedures are usually quite simple. The advantage of this is that it allows the theorem prover to be extended by users without the danger of them making the system unsound. In particular, a user does not have to be a logician to safely extend the system. If the user’s code is incorrect the worst that can happen is that the derived rules will fail; they cannot generate an invalid theorem. However, procedures for meta-theoretic properties are also critical code, so if meta-theoretic properties are used, the soundness of the system relies on the correctness of their implementations. This gap in the security can be plugged by proving the correctness of the implementations, but the proofs of correctness may be very difficult and to ensure security these proofs need to be transformed into new ‘primitive’ inference rules by some automatic means such as reflection (see Section 7). For many systems this requires sophisticated extensions to the logic.

In many applications the security of a theorem prover is not of critical importance. However, one of the major applications of mechanical theorem provers is in the verification of computer systems. In this field the soundness of the theorem prover is of considerable importance, and is a crucial requirement when the systems being verified are safety or security critical, e.g. nuclear powerstation controllers, fly-by-wire aircraft systems, and defence systems. For such applications it may be a requirement that the proof of correctness of the system be checked by a simple (and therefore easily verified) proof-checker that deals only with primitive inferences (see Section 32.2 of [MoD91]). In this case meta-theoretic properties cannot normally be used, since a full proof in terms of applications of primitive inference rules is required. An exception to this occurs when the meta-theorem is proved in a constructive meta-theory. The object-level proof can then be generated from the meta-level proof, but in doing so the performance benefits of meta-theoretic reasoning are likely to be lost.

In summary, then, theorem provers which fully expand proofs into primitive inferences are slower than other comparable systems, but are required for certain important applications. It has been claimed that fully-expansive theorem provers are orders of magnitude less efficient [Rus90]. However, we take the view that such systems are necessary, and so it is worth investigating what can be done to speed them up without compromising security. In this paper we present the results of the first stages of such an investigation. This has dealt with the problem of producing a practical proof procedure for a subset of arithmetic, where the procedure produces a proof entirely in terms of primitive inferences. We believe this is a good starting point for the investigation and has practical merit. We begin by outlining the reasons why proof procedures written for a fully-expansive theorem prover tend to be very slow. We then discuss how the choice of decision procedure is influenced by the need for a full object-level proof. We continue by describing in detail methods which help to avoid many of the inefficiencies that readily arise when writing proof procedures for a fully-expansive theorem prover. We give comparative results for arithmetic proof procedures with and without optimizations and discuss related and future work.

2 Unnecessary Inference

The work described in this paper is aimed at improving the efficiency of LCF-like theorem provers [GMW79] (which satisfy our definition of fully-expansive). In particular, the ideas have been implemented in the HOL system [Gor87]. The primitive inference rules considered are those of HOL. Results will of course vary to some extent with the particular primitive inference rules of the system being used.

In the previous section we described the computationally intensive nature of producing a proof in terms of primitive inferences. The extra computation is inherent in the detail of the proof and in the validity checks that are being performed for each primitive inference. However, much of the computation performed during automatic theorem proving does not contribute to the final theorem. Some of it is involved with searching for a proof and a lot is wasted. For example, primitive inferences performed down unsuccessful branches of a search are a major source of wasted computation. Primitive inference rules are applied down such branches because the simplest way to code the procedure is to integrate the search for a proof with the formal justification of the proof. We believe that separation of the search for a proof from the justification is critical for the efficiency of fully-expansive theorem provers. In partially-expansive systems such separation is far less important because fewer (if any) primitive inferences take place.

Integrated search and justification is a major source of unnecessary inference. However, it is not the only source. There are two main types of unnecessary inference:

• Unused inference

• Repeated inference

As we have said, unused inference often takes the form of inference done during search down a blind alley and which is later discarded because it does not contribute to the proof of the original conjecture. Unused inference is easily spotted when it is due to high-level aspects of the algorithms, but it can also occur at a low level due to the detailed implementation of the algorithms. A good example of this is rewriting. A depth rewrite of a term is the application of one or more rewrite rules at every subterm to which they are applicable. There are a number of varieties of depth rewriting. Some just try one pass over the term; others repeatedly pass over the term until no changes take place. The obvious algorithms for performing a depth rewrite of a term wander down the tree structure of the term applying the rewrite rules where possible. Any branches of the tree in which the rewrite rules do not apply are unchanged. In fact the obvious algorithms will rebuild such branches to produce a subtree identical to the original. This involves a large number of primitive inferences when in fact just one would suffice.

It is (relatively) cheap, though not necessarily simple, to avoid performing unused inference. Generally, all that is required is for the search to be separated from the actual inference, and only when the route to a proof has been found is the necessary inference performed. We describe how this may be implemented in Section 5.2.2. The other main type of unnecessary inference cannot always be avoided cheaply. To avoid repeated inference it is often necessary to keep track of the inferences that have already been performed. This tends to be very costly in terms of space, so there is a time-space trade-off to be made. Also, managing the information that keeps track of the prior inferences may be costly in time.

Proving the same lemma more than once is almost bound to happen during extensive use of a theorem prover. We do not propose trying to eliminate repetitions altogether, but only those which take place within the proof of a single conjecture, and even then, only if it is cost-effective to maintain the information required to detect the repetitions. Repetition may be due to badly organized control or it may be inherent in the problem. Inherent repetition is difficult to avoid. An example from arithmetic is the multiplication of constants. With a Peano axiomatization of numbers (i.e. a unary representation), simply multiplying two constants can require large amounts of logical inference. A given arithmetic proof may involve performing the same multiplication in several places. Given the large cost of doing these in such a system, it may well be worth trying to avoid the repetition. However, this involves maintaining a database of constant-multiplication theorems that have already been derived. See Section 5.3 for more about this. Repetition that is due to badly organized control is usually easier to deal with. A change to a more delicate algorithm may be all that is required.

3 Choice of Decision Procedure

Decision procedures for subsets of arithmetic are well known. The subset of arithmetic formulae made up from integer constants, integer variables, addition, multiplication by constants, integer relations (<, ≤, =, ≥, >) and the logical connectives (¬, ∧, ∨, ⇒, ⇔, ∀, ∃), was shown to be decidable by Presburger in 1929. Decision procedures are known for full Presburger arithmetic and these are also applicable to the smaller subset consisting of only those Presburger formulae which when placed in prenex normal form contain no existential quantifiers. However, faster procedures are known for the smaller subset. The best are of considerably smaller time complexity than those for full Presburger arithmetic. Since many arithmetic formulae which arise in verification proofs fall into the smaller subset [Sho77], it is probably advantageous in these applications to use a procedure for this smaller subset. Perhaps the best known is the SUP-INF method due to Bledsoe [Ble75] and improved by Shostak [Sho77].

Since the main application area of fully-expansive theorem provers is verification, we chose to investigate a decision procedure for the subset of Presburger formulae whose prenex forms do not contain existential quantifiers. Arithmetic is commonly used in verification proofs. In hardware verification, natural numbers are often used to represent time or steps in an execution.

There are significant differences between natural and rational arithmetic where decision procedures are concerned. For example, the SUP-INF method is complete for rational arithmetic, but not for natural arithmetic. This has to do with the fact that the method performs a computation in the rational domain and then attempts to interpret the result in the natural domain.

The fastest algorithms known for deciding the non-existential subset of Presburger arithmetic are not necessarily the most efficient when trying to prove a formula by primitive rules of inference. There are two reasons for this.

First, the cost of the primitive inferences may be so great in comparison with the other computation that the cost of the procedure is dominated not by the underlying algorithm but by the number of inferences performed. Thus a procedure which requires a small number of inferences may be much faster than one that has a faster decision algorithm but which requires a large number of primitive inferences to be performed.

Second, the computations may abstract away from the actual formulae, or assume properties that have to be dealt with explicitly in a fully-expanded proof^{1}. The SUP-INF method is a good example of this. Since it performs a computation in the domain of rational numbers, following the algorithm with primitive inferences would require that the natural number formula be ‘converted’ into an equivalent formula about the rationals. The algorithm performs some quite complex calculations on the rational numbers. Following the algorithm directly with inferences would entail symbolic execution (rewriting) of the logical formulae. This is very costly in a fullyexpansive theorem prover. In addition, a theorem for natural numbers would have to be derived by proof from the theorem for rationals^{2}, introducing yet more expensive inference.

The possibility still remains of using the SUP-INF method as an indirect guide for a proof by primitive inference. For example, if the method finds a counterexample to a formula, the formula can be refuted by substitution and evaluation (see Section 5.4 for details). However, in general some other means of guiding the proof directly is required.

The method of quantifier elimination described by Hodes [Hod71], and used by the Boyer-Moore theorem prover [BM88], works directly on the formula to be proved and does not involve the use of complex ‘meta’ calculations. It is therefore well suited to guiding primitive inferences. It is this method we use to show that by carefully avoiding unnecessary inferences much of the inefficiency of fully-expansive theorem provers can be overcome.

1In other words, the procedures may make use of meta-theorems.

2This is not in general possible, which is why the SUP-INF method is not complete for the naturals.

4 Our Version of Hodes’ Method

We now describe the proof procedure used to illustrate our claim that unnecessary inferences are significantly to blame for the apparent inefficiency of fully-expansive theorem provers. The procedure is based on Hodes’ method [Hod71].

The procedure first converts the formula of natural number arithmetic to be proved into prenex normal form, failing if the resulting formula contains existential quantifiers. The result is a formula of the form:

∀x_{1} … x_{n}. f[x_{1}, …, x_{n}]

The procedure then attempts to prove that ¬f[x_{1}, …, x_{n}] is false by normalizing it. If this normalized formula can be shown to be false, the validity of the original formula given as argument to the procedure is a straightforward consequence.

The normalization of a formula proceeds as follows. The implications and Boolean equalities are replaced by conjunctions, disjunctions and negations. The negations are then pushed as far down the term as possible and the term is put into disjunctive normal form. This yields a disjunction of conjunctions. The aim is to falsify this term, so each disjunct has to be shown to be false.

Each disjunct can be viewed as a set of inequalities. To show that a disjunct is false the procedure attempts to eliminate ‘variables’ from the set of inequalities. The elimination is done along the lines described by Hodes. Each element of a set of inequalities is a linear inequality or the negation of a linear inequality. They are converted to ≤ inequalities using rules such as:

(m < n) = (m + 1 ≤ n)
(m = n) = (m ≤ n) ∧ (n ≤ m)
¬(m > n) = (m ≤ n)

The resulting inequalities are normalized so that each variable appears at most once in the inequality, and on the appropriate side of the relation so that its coefficient is positive. The procedure then attempts to eliminate the variables by combining pairs of inequalities. For example, consider the following conjunction of inequalities:

(2m + 1 ≤ n) ∧ (3n + 2 ≤ m)

To eliminate n the first inequality can be multiplied by 3, and 2 added to both sides:

(6m + 5 ≤ 3n + 2) ∧ (3n + 2 ≤ m)

Transitivity then gives:

6m + 5 ≤ m

which is not satisfiable in the natural numbers.

The aim of this process of variable elimination is to prove that each set of inequalities is false. Unfortunately the procedure is incomplete because, in general, the steps of the elimination are implications, not equalities as in Hodes’ method. This is because we are working in the domain of natural numbers rather than rationals or reals. For example, the following is a theorem in the rational domain but not for natural numbers:

(∃n. m ≤ 2n ∧ 2n ≤ p) = (m ≤ p)

When m and p are both 1, there is a rational n that gives us this equality, but no natural number n. Since in the natural domain we only have the implication:

(∃n. m ≤ 2n ∧ 2n ≤ p) ⇒ (m ≤ p)

we can only prove anything about the original set of inequalities if we ultimately derive false. Deriving true tells us nothing. To put it another way, information may be lost as we proceed with elimination. When we eliminate a multiple of a variable we may produce a set of inequalities which is satisfiable even when the original set was not.

5 Avoiding Unnecessary Inference

In this section we describe in detail various methods for avoiding unnecessary inference in the context of proving formulae of linear arithmetic. We do not describe the proof procedure in full but concentrate on those features which are interesting with respect to proof by primitive inference.

5.1 Normalization

The following optimizations are used during the normalization process:

• Avoid rebuilding unchanged subterms

• Avoid repeated passes over the term

• Do low-level manipulations before splits occur

• Use compound rewrite rules, rather than several simple ones

• Avoid undoing previous changes

There is a close relationship between these optimizations. We do not claim great originality for the techniques. We are simply using them as illustrations of our claim that fully-expansive theorem provers can be made more efficient if care is taken when writing proof procedures. We briefly discuss the issue of ease of programming in Section 8.

To the best of our knowledge the idea of avoiding the rebuilding of subterms when rewriting is due to Roger Fleming of Hewlett Packard Laboratories, Bristol, England. The idea is to raise an exception^{3} when no change has occurred at a subterm. These exceptions are propagated back through the recursive calls of the ‘tree-walking’ function until a node is reached for which one or more of the branches has been changed. The unchanged branches then give rise to a theorem of the form ⊢ t = t where t is the term corresponding to the branch. As an example, consider removing double negations from the term:

(¬¬x) ∧ (y ∨ z)

The ¬¬x is transformed to x, but y and z remain unchanged. So, the left conjunct gives rise to the theorem:

⊢ ¬¬x = x

and the right conjunct gives rise to:

⊢ (y ∨ z) = (y ∨ z)

These can be combined using a rule of inference to give:

⊢ (¬¬x) ∧ (y ∨ z) = x ∧ (y ∨ z)

However, using a naïve algorithm, the second theorem would be generated by combining the theorems ⊢ y = y and ⊢ z = z, when in fact it can be generated directly. Direct generation saves several costly inferences, even for a simple example like this.

We have reimplemented Paulson’s conversions [Pau83] using this technique in such a way that the change is almost transparent to the programmer of the proof procedure. So, code written using Paulson’s versions requires very little change for it to have the same functionality with the optimized versions. Improved performance is gained at virtually no expense to the programmer. We discuss this further in Section 5.1.1. We have not yet been able to make the remaining optimizations transparent to the programmer. To use them the programmer has to think carefully about the order of application of conversions.

The cost of rebuilding terms is also the motivation for the second optimization. We should avoid repeated passes over a term if possible. Suppose that in the example above the x was actually the inequality (n + 1 ≤ 2n). This can be simplified to (1 ≤ n). The ‘obvious’ approach is to have a procedure which eliminates all double negations from a formula, and another procedure which dives down to the atomic propositions of a formula and simplifies any inequalities it finds. These two procedures can then be used in sequence to achieve full simplification. However, it takes considerably fewer inferences if the inequality is simplified on the same pass over the term as the one in which the double negation is eliminated. The conjunction then has to be rebuilt only once.

3Fleming’s implementation was for HOL88 and hence was written in ML [GMW79].

It is not always possible to do all the normalization on a single pass. A change at some node of the term may introduce the potential for simplification lower down in the term; potential that will be missed because the subterms have already been processed on this pass. Often these effects are fairly local, so a small amount of backtracking may be worthwhile. Careful analysis of the normalizations that are taking place should reveal these instances. There is an example of this in the normalization of arithmetical formulae. Having eliminated implications and Boolean equalities, negations are rippled down to the atomic propositions. Suppose that a negation gets moved down to the atom (m = n). While at an atom we want to normalize it to ≤ inequalities:

⊢ (m = n) = ((m ≤ n) ∧ (n ≤ m))

However, we now have a new conjunction through which we can move the negation:

⊢ ¬((m ≤ n) ∧ (n ≤ m)) = ¬(m ≤ n) ∨ ¬(n ≤ m)

Note that if m or n were more complex terms we might want to attempt to normalize them before using the rule for (m = n). If we do the normalization afterwards, it will take place twice for each of m and n, unless we introduce some mechanism for recording the first normalization of each. This is an example of where with a little care repeated inference can be avoided without introducing other costs. The whole example illustrates the third optimization: “Do low-level manipulations before splits occur”.

The example with ¬(m = n) can be optimized even further by making use of a compound rewrite rule. That is, instead of just having a rule for equalities we also have a rule for the negation of an equality:

⊢ ∀m n. ¬(m = n) = (m + 1 ≤ n) ∨ (n + 1 ≤ m)

This saves a few more costly inferences. It is a widely applicable technique which overall makes significant savings. The general idea is that the specialization of a theorem takes a fixed number of inferences per variable no matter what the form of the theorem. We should therefore use theorems which capture as much change as possible and thereby move some of the inferences out of the proof procedure and into the one-off proof of the theorem (the theorems used as rewrite rules in the procedure are preproved). This is the fourth of our optimizations and is an example of avoiding repeated inference in the sense that the compound theorem for rewriting is derived only once rather than every time the rewrite is applied.

Splitting also occurs when Boolean equalities are eliminated to form two implications:

⊢ ∀x y. (x = y) = (x ⇒ y) ∧ (y ⇒ x)

It might therefore seem sensible to normalize the atomic propositions (arithmetic relations) before eliminating Boolean equalities. However, after eliminating equalities, negations will be introduced:

⊢ ∀x y. (x = y) = (¬x ∨ y) ∧ (¬y ∨ x)

When rippled down to the atomic propositions these may cause the arithmetic expressions to be renormalized. This is an example of a breach of the final optimization, which is to avoid undoing work that has already been done. Here, unfortunately, we have a conflict between two of the optimizations. We can either normalize before splits occur and risk redoing work, or we can make sure we don’t have to renormalize but leave the possibility of the normalization being duplicated due to the expression being duplicated. Which optimization gives the better performance will depend on the formula to be proved.

It is obviously wasteful to undo changes, but it is not always easy to see that one normalization pass will undo the changes of a previous one. The best solution we can offer to this at present is careful thought on the part of the procedure implementor. It would be nice though if proof procedures could be written in a framework in which the system functions detected the waste for themselves and optimized it away.

5.1.1 Optimized Conversions

In this section we describe a reimplementation of Paulson’s conversions [Pau83]. The new conversions avoid rebuilding unchanged subterms and in doing so provide optimization of proof procedures in a way that is largely transparent to the programmer. The conversions use the raising and trapping of exceptions to avoid rebuilding the unchanged subterms.

The transparent change is achieved by changing the ‘specification’ of all conversions. Instead of expecting an equation of the form t = t to be returned when a conversion does nothing, we expect it to raise an exception. This means that at the very top level we have to be prepared to trap this exception and generate the theorem for t = t by a single primitive inference. However, we only do this when we absolutely must have a theorem, that is we have finished doing equational reasoning.

The exceptions are raised by the identity conversion ALL_CONV and by other conversions which can leave terms unchanged. Paulson’s ALL_CONV takes a term t and returns the theorem ⊢ t = t. Our version simply raises an exception with the string `QCONV`^{4}:

   let ALL_CONV t = failwith `QCONV`;;

(For a description of ML syntax see [Pau83]). The exception can be trapped at the top level using the function QCONV which has no analogy in Paulson’s implementation:

   let QCONV conv t = (conv t) ??[`QCONV`] (REFL t);;

The ‘??’ traps only those exceptions with the strings specified in the list following it. So QCONV applies the conversion conv to the term. If this does not fail (no exception is raised) the result becomes the result of the call to QCONV. If a `QCONV` exception is raised the primitive inference rule REFL is applied to the term to generate the theorem ⊢ t = t.

Conversions can be sequenced using THENC:

4The significance of the ‘Q’ in ‘QCONV’ is that exceptions are trapped using a question mark in the language ML.

   let THENC conv1 conv2 t =
    (let th1 = conv1 t
     in  ((th1 TRANS (conv2 (rhs (concl th1)))) ??[`QCONV`] th1))
    ??[`QCONV`] (conv2 t);;

((rhs (concl th1)) is the right-hand side of the conclusion of the theorem th1). The intended behaviour is for the first conversion conv1 to be applied to the term to give the theorem ⊢ t = t_{1}, followed by application of the second conversion to t_{1} to give the theorem ⊢ t_{1} = t_{2}. Transitivity is then used to generate the final result: ⊢ t = t_{2}.

In the implementation above, if the application of the first conversion does not change the term, an exception will be raised. This is caught by the trap in the last line, and the second conversion is then applied to the original term. However, we know that the first conversion left the original term unchanged, so the result will be correct, but it will be achieved without having to generate a theorem for the result of the first conversion. If the first conversion does change the term, but the second one does not, another failure trap causes the result of applying the first conversion to be returned as the full result.

The alternation operator on conversions, ORELSEC, is the most delicate of the new definitions. ORELSEC is meant to trap the real exceptions which are generated for reasons such as the term being of the wrong syntactic form for the first conversion:

   let ORELSEC conv1 conv2 t =
    (conv1 t) ?\s if (s=`QCONV`) then (failwith `QCONV`) else (conv2 t);;

Here we have to trap any exception raised from the application of the first conversion. The notation ‘?\s’ traps all exceptions and binds the failure string to the variable s. If the exception is `QCONV`, this exception is regenerated. Otherwise the result of the ORELSEC becomes the result of applying the second conversion to the original term. So, ORELSEC applies the first conversion and if this fails for a real reason the second conversion is applied instead. If the first conversion simply leaves the term unchanged then the `QCONV` exception used to indicate this is allowed to propagate.

So, ORELSEC and the other conversions produce the same results as Paulson’s versions, provided the exception `QCONV` is not used by the programmer for anything other than its intended purpose. The choice of name for the exception makes misuse highly unlikely even if the programmer is unaware of the special significance of

`QCONV`.
   Once the basic conversions such as ALL_CONV, NO_CONV, REWRITE_CONV, SUB_CONV,

THENC and ORELSEC have been modified, the code for Paulson’s depth conversions remains unchanged since these conversions are implemented in terms of the basic conversions. More importantly, this also applies to users’ code.

One way in which the technique is not a transparent change is if the programmer wishes to perform some special operation within a conversion as opposed to building it entirely from other conversions. The possibility of an exception being obtained rather than a theorem then has to be taken into account. Of course, the programmer could use the function QCONV, but that would destroy the optimization.

5.2 Variable Elimination

5.2.1 The Elimination Process

Avoiding unnecessary inference during variable elimination can be achieved by separating the search for a proof from the inference required to generate a theorem.

We have a set (conjunction) of inequalities that we hope to be able to prove false. If any of the inequalities contain only constants, they can be evaluated directly to either true or false. A false inequality completes the proof. A true inequality can be discarded. We are then left with a set of inequalities such as:

(m + n ≤ p) ∧ (2m ≤ 1 + n) ∧ (3 + p ≤ 3m)

Suppose we decide to eliminate m. We compute the lowest common multiple of all the coefficients of m, and multiply the inequalities by constants so that the coefficients become that value:

(6m + 6n ≤ 6p) ∧ (6m ≤ 3 + 3n) ∧ (6 + 2p ≤ 6m)

We then form all the possible pairs of inequalities such that one of the pair has m on the right-hand side and the other has m on the left:

(6 + 2p ≤ 6m) ∧ (6m + 6n ≤ 6p)
(6 + 2p ≤ 6m) ∧ (6m ≤ 3 + 3n)

Addition of terms to both sides of selected inequalities then allows us to use the transitivity^{5} of ≤ to eliminate m:

(6 + 2p + 6n ≤ 6p)
(6 + 2p ≤ 3 + 3n)

We know that both of these inequalities are true assuming the original set of inequalities, so simplifying we get:

(6 + 6n ≤ 4p) ∧ (3 + 2p ≤ 3n)

Similarly, we can eliminate n:

(6 + 6 + 4p ≤ 4p)

from which we get:

(12 ≤ 0)

which in turn evaluates to false.

In the example above both of the initial pairings were used in the derivation of false. In general this is not the case. Some of the pairings may not contribute. This is why it is important to separate the search from the actual proof. We may need to investigate a pairing that does not contribute in order to keep the options open for later eliminations, but we don’t want to do the logical inference.

5Note that to use transitivity the right-hand side of the first inequality must be identical to the left-hand side of the second. Some kind of normalization such as sorting on the names of the variables must be used.

5.2.2 Using Higher-Order Functions

For a theorem prover written in a functional programming language like ML the search can be separated from the theorem-generation by use of higher-order functions. The idea is to use terms (rather than theorems) during the elimination process, but in addition to having terms in the arguments and results of the functions, we have a function as part of the data. This function is capable of performing the primitive inferences that prove (generate a theorem for) the transformations. For example, a proof function in a fully-expansive theorem prover might normally have the meta-language type:

     thm → thm

This is a function which given a theorem as argument, returns a theorem as its result. In the scheme we propose, the following type would be used:

     (term × (void → thm)) → (term × (void → thm))

This is a function which takes as its argument a pair (tm, f) of a term and a function. The function f is a ‘lazy theorem’. It takes an element of type void (which is a type with only one element) and returns the theorem corresponding to the term tm. The void argument delays evaluation so that the primitive inferences required to prove the theorem are not executed. Only when f is applied to the element of type void does the execution take place. There is no need to execute the theorem-generating functions immediately because the term tm can be used by the searching algorithms to find a proof.

The result of the proof function is another pair (tm′, f′) for the new theorem. The function not only manipulates the term tm to generate tm′, it also constructs the new ‘lazy theorem’ f′ from f by including calls to the primitive inference rules required to go from tm to tm′. However, these calls are not executed when f′ is constructed. They go into the body of f′ to be executed only when f′ is applied to an argument. So, if the path of the search later turns out to be unfruitful, f′ can be discarded and the primitive inference rules for the step will never be executed.

The main proof function is a higher-order function because it takes another function as an argument and returns a function in its result. The types of the argument and result may not in practice be exactly as we have shown them here, but the types given here illustrate the idea.

So, returning to the variable elimination procedure, when we find an elimination route that leads to false, we discard the unwanted functions (‘lazy theorems’) along with the unwanted inequalities, and only ‘execute’ those functions which are required to prove the conjecture.

5.2.3 Why the Optimization is Effective

In a fully-expansive theorem prover the execution of the theorem-generating functions is typically the dominant part of the computation. So, reducing the number of inferences performed has considerable efficiency benefits. Most theorem provers would not be doing the theorem-generation step at all. Finding an elimination path which leads to false would be considered sufficient.

To reiterate, then, the optimization we are claiming is not the cutting-down of the search space, but is the significant reduction in number of primitive inferences performed when the search for a derivation of false is separated from the proof of theorems which securely record the fact. Even then, generating a theorem by following the successful elimination path is not a trivial operation to program efficiently. Care needs to be taken not to waste inferences in operations such as reordering the conjuncts of a conjunction.

5.2.4 Further Optimization and Security

We can in fact optimize the search process as well. Provided the inequalities are first placed in a normal form, then for search purposes, we can represent each inequality not by a term but by a coefficient list such as:

                         (-1, [(`m`,-3); (`n`,1)])

This coefficient list represents the term: 1 + 3m ≤ n. It is an abstraction which discards all the unnecessary structural information. Computation on coefficient lists is far faster than the equivalent computation on terms. Properties such as associativity and commutativity become implicit. This can be thought of as exploiting meta-theoretic properties during the search while retaining the ability to do full object-level inference.

The computation for the search is not secure. However, an error in the coding of this search procedure cannot lead to a non-theorem being proved because when the associated proof function is executed it will fail. Thus, an error could lead to additional incompleteness of the procedure but it cannot make it unsound.

The search can stop as soon as it finds a way of deriving false, so the whole search space may not be investigated. This provides a small performance gain, but the real gains are due to the inferences saved. Hodes suggests choosing the variable to eliminate at each stage based on the number of pairings that would be generated relative to the number of original inequalities. This helps to avoid the blow-up that can occur in certain cases. Note that there may be inequalities that are not involved in the pairing because they do not contain the variable being eliminated. These inequalities are passed forward unchanged to the next stage.

It is unclear whether it is best to compute the lowest common multiple of all the coefficients of the variable to be eliminated, or to deal with each pair of inequalities separately. The former may lead to larger coefficients and the latter to more multiplications being necessary. As described in the next section, both of these situations can be costly in terms of number of primitive inferences.

5.3 Multiplication of Constants

If a unary representation for natural numbers is used in the theorem prover, computation times for secure arithmetic operations on constants are at best large and at worst impractical. The times depend on the size of the numbers themselves. Consider, for example, evaluating the sum (3 + 4) by formal proof. The transformations are:

     SUC(SUC(SUC(0))) + SUC(SUC(SUC(SUC(0)))) =
     SUC(SUC(SUC(0)) + SUC(SUC(SUC(SUC(0))))) =
     SUC(SUC(SUC(0) + SUC(SUC(SUC(SUC(0)))))) =
     SUC(SUC(SUC(0 + SUC(SUC(SUC(SUC(0))))))) =
     SUC(SUC(SUC(SUC(SUC(SUC(SUC(0))))))) =

where SUC is the successor function (it adds 1 to its argument). The transformations require significant amounts of inference.

The situation is even worse for multiplication^{6}. Consider:

2 ∗ 3 = SUC(1) ∗ 3 = (1 ∗ 3) + 3 = …

Here we have n recursive calls to the multiplication routine (where n is the value of the first argument) and n additions of the second argument to a partial result.

There is no way to avoid large computation times for secure proof on unaryrepresented constants, but there are ways to reduce the amount of inference required. For multiplying constants we use a version of the multiplication routine which remembers theorems for the multiplications it has done previously. This should be fruitful because it is likely that the same numbers will be involved in several calls. This use of “memo” functions is described by Michie in [Mic68]. It is similar to the notion of a cache in hardware design.

Multiplication is used during the normalization process and in particular when forming the weighted sum of two inequalities. In the latter case it is not hard to see that there are likely to be a lot of repeated calls. Thus this is a case of trying to avoid repeated inference.

Observe that when multiplying the inequality (m + 2 ≤ 3n) by 3, we first prove ⊢ 1 ∗ 3 = 3, then ⊢ 2 ∗ 3 = 6. However, the call to prove the latter theorem makes a call to prove ⊢ 1 ∗ 3 = 3. We have already proved this (and saved the result). Similarly the proof of ⊢ 3 ∗ 3 = 9 requires the proof of ⊢ 2 ∗ 3 = 6. So, by recording multiplication theorems we not only gain for multiplications we have done before, but also for new ones which make recursive calls.

For multiplications in which one of the arguments is 0 or 1, we can simply instantiate one of the following theorems:

⊢ ∀n. 0 ∗ n = 0  ⊢ ∀n. n ∗ 0 = 0  ⊢ ∀n. 1 ∗ n = n  ⊢ ∀n. n ∗ 1 = n

6We abbreviate SUC forms with numeric constants.

and we never store theorems of this form. We also don’t store both a theorem and a commuted version of it since it is relatively cheap to derive one from the other. Extra costs are incurred in storage space and in time to search the database of theorems, but in general these costs are outweighed by the benefits.

A similar technique could be used for addition of constants, but we suspect that the overheads are unlikely to be worth the benefits in this case. Also, it may be advantageous to maintain the database only for the duration of one call to the main arithmetic proof procedure. A different collection of constants is likely to be present in the next call, so the database may be of little use, and we must prevent it from becoming too large, else the maintenance and searching overheads will become excessive.

Formulae involving constants of any significant size cannot be processed in a practical amount of time because of the unary representation. However, this is the fault of the underlying representation, not of the procedure. It is a separate issue as to whether some other number system should be adopted or whether security should be compromised by trusting the machine’s arithmetic. These issues are beyond the scope of this paper.

5.4 Proving Formulae False

Shostak’s version of the SUP-INF method [Sho77] can be used to refute invalid formulae as well as to prove valid ones. When proving a valid formula the SUP-INF method is of no use for guiding a fully-expanded proof. However, for an invalid formula the method exhibits a counter-example. This counter-example can be readily used to obtain a fully-expanded proof that the formula is false; it is simply a matter of showing that there exists instances of the variables for which the body of the prenex normal form of the formula is false. Instantiation with the counter-example obtained by the SUP-INF method, followed by symbolic evaluation does just this. For example, consider the following invalid formula:

∀m n p. m < n ∧ m < p ⇒ n < p

The SUP-INF method can be used to obtain the counter-example: m = 0, n = 1, p = 1. Substituting these values into the formula we get:

0 < 1 ∧ 0 < 1 ⇒ 1 < 1

which evaluates to false. The counter-example can thus be used as a witness for the formula:

∃m n p. ¬(m < n ∧ m < p ⇒ n < p)

which is itself equivalent to:

¬(∀m n p. m < n ∧ m < p ⇒ n < p)

This is a situation in which insecure computation can be used to indirectly guide a secure proof by behaving as an ‘oracle’. No theorem-generation need be performed while searching for a counter-example.

Unfortunately Shostak’s SUP-INF is not complete for invalid natural number arithmetic formulae, and whereas the method is complete for most valid natural number arithmetic formulae that arise in verification proofs, we have encountered many typical invalid formulae which the SUP-INF method cannot refute unless it is allowed to do an exhaustive search (see [Sho77]).

6 Results

We have tested the proposed optimizations by writing a proof procedure for linear arithmetic in the HOL system. The HOL system [Gor87] is an interactive proof assistant for a classical higher order logic. It has been used for, amongst other things, hardware verification, protocol verification, and program refinement. HOL is a derivative of LCF [GMW79] and has retained the LCF methodology: the system consists of a higher-order functional programming language, ML, which is so called because it is the meta-language of the system. The language allows abstract datatypes to be defined. Built into the meta-language of the HOL system are abstract datatypes for logical types, logical terms and theorems. The abstract datatypes encapsulate the underlying tree structures with syntactic and semantic restrictions.

Since HOL is largely interactive, the arithmetic procedure will typically be called manually to prove a lemma or simplify an arithmetical expression within the current goal (formula to be proved). Thus the issues of integrating a decision procedure for arithmetic within an automatic system (see [BM88]) are not directly relevant here. However, these issues would arise if HOL were to become more automated.

We have compared the performance of our implementation with a similar proof procedure written by Albert Camilleri in 1985/86^{7}. Camilleri’s procedure is an experimental prototype. It was not intended as a final implementation but as a means of generating data on the performance of such proof procedures, and thereby to contribute to research on how proof procedures should be implemented in fullyexpansive theorem provers. It is in just this way that we use it.

It is only fair to point out that the functionality of the two procedures is not identical, so the comparison cannot be exact. However, the behaviours of the two implementations are very similar, so the timing figures are informative. The alternative would have been for us to write a proof procedure deliberately avoiding optimizations, so that some idea of the benefits of the optimizations could be obtained. However, this would have been open to the criticism that the inefficient procedure was contrived to show the optimizations in a good light. We think the comparison with Camilleri’s procedure is more realistic. The timing figures for our procedure are interesting in themselves since they give a feel for the practicality of the procedure.

7Private communication.

In Camilleri’s procedure much of the proof is done by depth rewriting, a technique now known to be inefficient in most cases. Even without efficiency optimizations throughout the program, on today’s machines Camilleri’s implementation can prove simple arithmetic theorems faster than the average user is likely to be able to using the system interactively. The program typically takes between a minute and two minutes on a large Sun 3. The data from 1985/86 suggests that the procedure was about five to six times slower than this on the machines of the day.

In contrast, for simple arithmetic theorems, the implementation using the optimizations suggested in this paper usually completes in under ten seconds on a Sun 3. This is a good order of magnitude faster than Camilleri’s unoptimized procedure. We believe that ten seconds is about the limit of most people’s patience, and ideally a program which leaves the user idle should complete in under a second. The user will then hardly notice any delay. Of course, for non-interactive use, i.e. when being called by another procedure, a program can never be fast enough.

Table 1 gives examples of timings in HOL88 Version 1.12 built under Franz Lisp and running on a Sun 3/160. We did not do the comparison in the latest version of HOL88 because this has the transparent optimization described in Section 5.1.1 built into the system, significantly increasing the performance of Camilleri’s procedure.

The table should be interpreted as follows: ‘Run’ is the run time in seconds. ‘GC’ is the garbage collection time in seconds. ‘PInfs’ is the number of applications of primitive inference rules used to prove the theorem. For each example there are two sets of figures. The figures labelled ‘U’ are for the unoptimized procedure and those labelled ‘O’ are for the optimized procedure.

The garbage collection times for individual theorems should not be taken too seriously since part of the garbage may have been generated by previous calls, or garbage generated by the call may not collected during the call. The former gives rise to misleadingly large garbage collection times, and the latter to times which are smaller than they should be.

The file of examples ranges from very simple formulae to (more typically) formulae of a similar complexity to the individual examples in the table. Note that for the unoptimized procedure the file had to be processed in three parts due to exhaustion of a particular Lisp resource. The figures given are the sums of the results for the three parts.

The number of equality symbols appearing in the formula has a very significant influence on the execution time because during normalization each Boolean equality is split into two implications, and each numeric equality is split into two inequalities. Thus, the size of the formula tends to be doubled for each equality symbol. This makes normalization slower and leads to a dramatic increase in the number of variable eliminations which have to be performed.

A side issue to the main point of this paper, but one which may be of interest to some readers, is the completeness of our procedure. First, it does not (and is not intended to) prove invalid formulae false. Second, we have only encountered one naturally-occurring valid formula (within the specified subset of linear arithmetic) which the procedure failed to prove:

∀m n. ¬(SUC(m + m) = n + n)

Run  GC PInfs
File of 54 examples  U 6001.3 1437.5 921782
O 212.5 165.8 21571
(n ≤ p) ∧ (p ≤ q) ∧ (q ≤ r) ∧ (r ≤ s) ∧ (s ≤ n) ⇒ U 537.2 102.2 76872
(n = q) O 5.9 3.5 495
(m = n) ∧ (n = p) ⇒ (m = p)  U 322.2 67.5 46094
O 4.6 3.4 423
(n ≤ 4) ⇒ ((11 ≤ 3 ∗ n) ⇒ (n ≥ 4))  U 127.2 29.1 20387
O 2.3 3.4 275
¬(n ≤ p + m) ⇒ ((m + SUC(p) ≤ n) ∨ (m ≤ 0)) U 100.3 20.8 15902
O 2.2 3.5 205
(m < n) ∧ (n ≤ p) ⇒ (m < p)  U 80.5 15.7 11915
O 2.2 0.0 210
((m ≤ n) = (n ≤ m)) = (m = n)  U 662.7 138.6 98928
O 24.6 20.6 2220
(m < n) ∧ ¬(SUC(m) = n) ⇒ (SUC(m) < n)  U 183.4 41.1 28699
O 3.4 0.0 322
(m ≤ p) ∧ (n ≤ q) ⇒ (m + n) ≤ (p + q)  U 104.9 24.0 15872
O 2.8 3.4 249
(m ≤ n) = (2 ∗ m) ≤ (2 ∗ n)  U 133.4 30.2 21322
O 5.0 3.5 525
n ∗ 3 = n + (n + n)  U 33.6 12.2 5678
O 1.5 3.4 152

Table 1: Comparison of Unoptimized and Optimized Procedures After normalization this leaves us with the following conjunction of inequalities to prove false:

∃m n. (1 + (2 ∗ m)) ≤ (2 ∗ n) ∧ (2 ∗ n) ≤ (1 + (2 ∗ m))

Eliminating the (2 ∗ n) by transitivity leads to a true statement, whereas the statement above is false in the natural number domain because (2 ∗ n) (an even number) is being constrained by the inequalities to be equal to (1+(2∗m)) (an odd number). This is discussed in Section 4.

Of course, since we know at least one reason why the procedure is incomplete it is quite easy to contrive examples for which the procedure fails.

We have tested the procedure on some larger examples and have been pleasantly surprised to find that not only can the procedure prove them, but also that the computation times are not excessive. An example is:

(m = 1) ∧ (n = 2) ∧ (p = 3 ∗ n) ∧ (q = p + 2) ⇒
((m + (5 ∗ n) + (2 ∗ p) + (3 ∗ q)) = ((p ∗ 6) + q + m + n))

which (including garbage collection time) was proved in around 26 seconds.

7 Alternative Approaches

Techniques like those described in this paper are not the only way to obtain reasonably efficient secure proof. Howe [How88] describes the internalization of a portion of a theorem prover’s meta-theory and the use of a partial reflection mechanism as an alternative to using primitive inferences for all proof. The idea is to prove the implementation of a proof procedure correct within the prover’s logic and then use the procedure directly, rather like a new primitive inference rule. This is sound by virtue of the correctness proof, and has been investigated in a number of theorem provers. See for example [BM81].

As Howe says, reflection has the advantage that it is far more efficient then using primitive inferences, and indeed it will not be possible to make the use of primitive inferences as efficient. However, the reflection approach has not yet been shown to be viable in general. The main problem is having to prove the correctness of the proof procedures, which involves representing and proving properties about the data-structures used in the implementation of the theorem prover.

The straightforward primitive inference approach has the advantage that with suitable encapsulation of the critical code we do not have to worry about the correctness of proof procedures. If there is an error in a procedure, the procedure may fail, but the error cannot make the system unsound. Amongst other things, this allows us to use very sophisticated heuristics without having to prove their correctness.

8 Contribution and Future Work

In this paper, we have described a number of techniques for improving the performance of proof procedures in fully-expansive theorem provers. The real contribution of this work is the application of the techniques to fully-expansive theorem provers, in which their benefits are considerably greater than in most other theorem provers. In fully-expansive theorem provers execution times are usually dominated not by the search for a proof but by the (secure) generation of the theorem. In most theorem provers, the formula to be proved is processed by various algorithms until it has been reduced in such a way that it is known (by the implementor) to be true. In a fully-expansive theorem prover this is only the first step. The second step is to use the ‘proof’ to generate the theorem by applications of primitive inference rules.

Typically it is the second stage which dominates the computation, so normal techniques for optimizing theorem proving may have little effect on the performance of a fully-expansive theorem prover. Furthermore, the optimizations often take advantage of implicit information and meta-theoretic properties. Use of these may make the ‘proof’ useless for generating the theorem since there is no indication of what primitive inferences need to be performed.

The techniques we have described are effective not because they dramatically cut down the search space (some don’t even affect the search space) but because they avoid unnecessary inferences in the second stage of the computation. These two issues are strongly related but are not the same.

Proof procedures in fully-expansive theorem provers are usually written using theorems as the underlying data structure rather than terms. When search for a proof is involved this can be very wasteful, since primitive inference rules are applied during the investigation of the blind alleys, and these applications usually involve significant checks that the rule really is applicable. The rules need only be applied down the successful search path in order to generate the theorem. As we have shown (Section 5.2.2), higher-order functions can be used to separate the two stages of computation without having to physically separate the code.

There is a limit on how much performance can be gained in a fully-expansive theorem prover by avoiding unnecessary inference. Much of the cost is inherent in the primitive inferences and is a price that has to be paid for the security. ‘Reflection’ offers the possibility of highly efficient verified proof procedures, but has its own problems: Proving the correctness of the proof procedures may be very difficult. In addition, some applications may require a proof in terms of primitive inferences.

Whether reflection proves successful or not, we believe the issues addressed in this paper are important considerations when dealing with a fully-expansive theorem prover, because it is unlikely that all proof procedures will be verified. Users are likely to want to develop their own high-level procedures without having to prove their correctness. On the other hand, the techniques described in this paper will only be of real benefit to the user of a fully-expansive theorem prover if they can be implemented relatively simply. It is therefore a goal of future research to develop more general techniques and to push as much of the work as possible into system functions. Then, provided the programmer makes use of these functions for writing proof procedures, much of the unnecessary inference will be eliminated transparently.

A potential problem with developing transparent optimizations is that optimization techniques can be heavily interrelated. The introduction of an optimization may influence the effectiveness of some other optimization, even to the extent of making it a de-optimization. Since this may all depend on real execution times of various system functions, it seems unlikely that an automatic solution will be possible for arbitrary user-suggested optimizations.

Another interesting issue to be considered is to what extent the integration of one proof procedure with another affects the optimization techniques described in this paper. For example, some of the optimizations for the normalization process described in Section 5.1 are heavily dependent on the form of the terms being processed. Extending the basic arithmetic operations with functions from other theories might well have an effect on the optimizations.

Acknowledgements

I would like to thank Albert Camilleri of Hewlett Packard Laboratories, Bristol, England, for generously providing access to the linear arithmetic proof procedure he wrote while a student at Cambridge University, and for pointers into the literature.

Thanks also to Mike Gordon for his support, encouragement and advice, and for comments on earlier versions of this paper. Tom Melham has taught me a great deal about theorem proving in the HOL system, both directly and through reading his code. Malcolm Newey encouraged me to develop a linear arithmetic procedure for HOL, and directed me to the literature. Robert S. Boyer also provided useful references and suggestions.

This research was supported by the Science and Engineering Research Council of Great Britain in the form of a studentship to the author.

References

[Ble75] W. W. Bledsoe. A new method for proving certain Presburger formulas. In Advance Papers 4th Int. Joint Conf. on Artif. Intell., Tbilisi, Georgia, U.S.S.R., pages 15–21, September 1975.

[BM81] R. S. Boyer and J S. Moore. Metafunctions: Proving them correct and using them efficiently as new proof procedures. In R. S. Boyer and J S. Moore, editors, The Correctness Problem in Computer Science, pages 103–184. Academic Press, 1981.

[BM88] R. S. Boyer and J S. Moore. Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic. Machine Intelligence, 11:83–124, 1988. Edited by J. E. Hayes, D. Michie and J. Richards. Oxford University Press.

[GMW79] M. J. Gordon, A. J. Milner, and C. P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.

[Gor87] M. J. C. Gordon. HOL: A proof generating system for higher-order logic. Technical Report 103, University of Cambridge Computer Laboratory, 1987. Revised version in G. Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, Kluwer, 1987.

[Hod71] L. Hodes. Solving problems by formula manipulation. In Advance Papers 2nd Int. Joint Conf. on Artif. Intell., London, pages 553–559. The British Computer Society, September 1971. Revised version in Artificial Intelligence 3, North-Holland, Amsterdam, 1972, pages 165–174.

[How88] D. J. Howe. Computational metatheory in Nuprl. In Proceedings of the 9th International Conference on Automated Deduction, Lecture Notes in Computer Science, Volume 310, pages 238–257. Springer-Verlag, 1988.

[Mic68] D. Michie. “Memo” functions and machine learning. Nature, 218:19–22, 6th April 1968.

[MoD91] Interim defence standard 00–55: The procurement of safety critical software in defence equipment, part 2: Guidance. Ministry of Defence, Directorate of Standardization, Kentigern House, 65 Brown Street, Glasgow, G2 8EX, UK, April 1991.

[Pau83] L. Paulson. A higher-order implementation of rewriting. Science of Computer Programming, 3:119–149, 1983.

[Rus90] J. Rushby. Formal methods and critical systems in the real world. In D. Craigen and K. Summerskill, editors, Formal Methods for Trustworthy Computer Systems (FM89), pages 121–125. Springer-Verlag, 1990. Section 1 of Appendix C.

[Sho77] R. E. Shostak. On the SUP-INF method for proving Presburger formulae. Journal of the ACM, 24(4):529–543, October 1977.