When we have a set of conjectures formulated in a common language and proved from a common set of axioms using an automated theorem prover, it is often possible to automatically construct lemmas that can be used to prove the conjectures in a shorter time and/or with shorter proofs. We have implemented a system that repeatedly tries to improve the set of assumptions for proofs of given conjectures using lemmas that it extracts from the proofs constructed by an automated theorem prover. In many cases it can significantly reduce the total time or the overall sum of the lengths of the proofs of the conjectures. We present several examples of such sets of conjectures and show the improvements gained by the system.
Imagine a professor of mathematics who gives the same lectures every year. She works in a standard theory and she has a fixed set of theorems that she wants to present and prove every year during the course. And because she wants to save her and her students’ time, she would like to have as efficient proofs as possible. She would like to find such lemmas that would shorten the total time she has to spend for presenting the proofs.
Our aim will be to search for lemmas in such environment and try to use them to make the proofs of conjectures more efficient.
Finding useful lemmas has of course much more serious applications, namely reducing the amount of resources necessary to prove a particular set of conjectures or to prove conjectures that could not be proved without such lemmas.
Currently the system only restructures and compacts the proofs and doesn’t handle conjectures that the prover was not able to prove at the beginning. It can only improve existing proofs. In future we hope to be able to also search for proofs of the conjectures that couldn’t be proved from the initial set of assumptions.
The idea of an automated discovery of lemmas or theorems is not a new one. There were many different approaches to solve this task.
Owen L. Astrachan and Mark E. Stickel [AS92] used the idea of reusing lemmas to speed up a model elimination theorem prover.
Art Quaife [Qua92] used Otter [McC94] to prove many fundamental mathematical theorems. He included the theorems he had already proved as assumptions for the more complicated ones. The sequence in which the theorems were proved was determined by Quaife, based on his mathematical knowledge.
Marc Fuchs, Dirk Fuchs and Matthias Fuchs sought for lemmas using genetic programming to improve tableau-based proof search [FFF99].
The HR system [Col02a], named after mathematicians Hardy and Ramanujan, uses a model generator to construct models based on a set of axioms, attempts to formulate conjectures and then prove them using an automated theorem prover. A brief description can be also found in [Col02b].
Larry Wos and Gail W. Pieper describe the technique of lemma adjunction in [WP03] and also discuss many different approaches for evaluating lemmas.
Article [SGC03] summarizes many different criteria for constructing and identifying quality lemmas. Humans generally use the inductive approach – from many similar problems they try to induce a more general conjecture. This approach requires good knowledge of the particular field of mathematic and also good mathematical intuition. Another approach described is generative, when more sophisticated techniques (for example syntactic manipulation) are used to construct new conjectures. An example of such a system is the HR [Col02b] program. The manipulative approach tries to construct interesting conjectures from already existing theorems. Finally, the deductive approach tries to automatically construct many logical consequences from a set of axioms using an automated theorem prover and then filter them and pick those that are interesting for the researcher.
The authors of [SGC03] also categorize different possible filters for interestingness. The filters include non-obviousness, novelty, suprisingness, intensity and usefulness.
Our approach is somewhat different from those mentioned above. It lies in between the manipulative and the deductive approach. We observe proofs of all the given problems and identify lemmas that are common to many of the proofs. The filter we develop and use for selecting good lemmas falls into the usefulness category - our measure is, how much each lemma could contribute to the proofs of other conjectures. Unlike other measures, this one can easily be evaluated by comparing different proofs conducted by the prover.
The lemmas that we produce are therefore interesting from the point of view of a machine. Hence, this can give us an interesting comparison between human and machine opinions on the usefulness of a lemma.
The ideas in the article [SGC03] and personal communication with many other researchers inspired our work which we present in this paper together with the empirical results we have obtained. 3
In sequel we assume that a consistent theory is given with some (possibly infinite) set of axioms. All the formulas we work with are formulated in the language of the theory and the conjectures that are to be proved and the lemmas that are constructed are proved using axioms selected from the axioms of the theory.
The systems starts by proving the conjectures one by one. The proofs of the conjectures that were successfully proved are then analyzed by the system. Formulas that appear multiple times in the proofs are then used as additional assumptions when looking for less costly proofs of the conjectures. The system tries to optimize the set of such formulas. We will call such formulas lemmas. 3.1
Let us first define some basic notions we will use throughout the text.
Notation 1 (Axiom, conjecture, lemma, proof) By an axiom we understand either an axiom of the underlying theory or a well known theorem of the theory that we use as an assumption.
A conjecture is a formula given on the input that is to be proved by the system. The system tries to find the most efficient proof of the conjecture using different sets of assumptions. Each such a set can contain some of the axioms, other conjectures or lemmas.
A lemma is a formula constructed by the system that is proved in a similar fashion as the conjectures are, and is used to improve the proofs of the conjectures or the proofs of other lemmas.
A proof is an output of a successful run of the prover. As we use a single theorem prover with the same settings on every run, the proof only depends on the conjecture being proved and on the set of assumptions being used.
The aim of the system is to find such lemmas and such sets of assumptions for the conjectures and the lemmas that either the total time required to prove the conjectures and the lemmas or the overall size or length of the proofs is minimized. 3.2
Initially, the system is given a set C of conjectures and for each conjecture C from C the system is given an initial set of assumptions AC. The set AC consists of a subset of axioms of the underlying theory and (possibly) of some other conjectures from C.
The idea is that the proofs of conjectures in C need not use the set of all the axioms of the theory (which might be infinite) and that some other conjectures from C might be useful. The user may have his own idea, which conjectures to add as assumptions to AC.
In the process of computation the system tries to optimize the set of lemmas and for each lemma the set of its assumptions. 3.3
At the end the system outputs the conjectures given at the input along with the lemmas that participate in the fastest/shortest set of proofs. For each conjecture and each lemma it outputs the optimal set of assumptions it has found, in the sense described later. 4
In our example we use a commonly used encoding to encode an axiomatization of propositional logic into terms, thus forcing the prover to use only the specified axioms and rules for inferences.
Then we use the system to prove some basic propositional theorems.
Note that the automated theorem provers were already used to look for interesting axiomatics of propositional logic, for example [MVF+02]. However, our aim is not to look for a new or otherwise interesting axiomatic, we use the system to optimize the proofs of several theorems.
We will denote the code of a formula by an over-line. For example for a propositional formula ϕ we denote the term that codes it by ϕ. Negation is coded by a unary function n and implication is coded by a binary function i. The fact that ϕ is a theorem ⊢ ϕ is coded by a unary predicate t. The following table summarizes the codes: ¬ϕ n(ϕ) ϕ → ψ i(ϕ, ψ) ⊢ ϕ t(ϕ) We use “→” just for implication in propositional logic we are coding. We use “⇒” for implication in predicate logic in which the conjectures are presented and in which the prover actually works. Thus the statement “if ϕ is provable then ψ → χ is provable” would be coded as t(A) ⇒ t(i(B,C)).
In order to increase the difficulty of the task we’ve used Meredith’s single axiom for propositional logic. It has only a single axiom schema and a single rule.
The axiom schema is defined for any formulas ϕ, ψ, χ, ξ and η, but the theorem prover computes with their codes, which are represented by the variables A, B, C, D and E in the language of the theorem prover. As these variables are universally quantified, the prover can replace each variable by any coded formula. The same applies to the coded modus ponens rule.
The coded representations of the schema and the rule are:
Meredith: ⊢ ((((ϕ → ψ) → (¬χ → ¬ξ)) → χ) → η) → ((η → ϕ) → (ξ → ϕ)) t(i(i(i(i(i(A, B), i(n(C), n(D))),C), E), i(i(E, A), i(D, A)))) MP: ϕ, ϕ → ψ ⊢ ψ
(t(A) ∧ t(i(A, B))) ⇒ t(B) This set of axioms was used as the initial set of assumptions for all the conjectures. No other dependencies between the conjectures were specified. The system was let to discover all the lemmas by itself from the proofs of the conjectures.
Table 1 shows the conjectures whose proofs the system was improving. The conjectures were proved using E prover[Sch02]. The cost of the proofs was measured in the number of processed clauses. This measure closely corresponds to the time the prover spends on a problem, but it is not dependent on the hardware the prover runs on. In the second column the conjectures are presented in their coded form. The third column shows the number of processed clauses the prover spent on each of the conjectures if they were proved only using the original assumptions. The fourth column shows the cost of the proofs after the system had finished the improvements using lemmas generated from the proofs. Note that to obtain the total cost of the final proofs we also have to include the cost of the proofs of the generated lemmas. The full listing of the generated lemmas is included in Table 10. As we can see, the total cost of proofs needed to prove the conjectures in this case was reduced to 3%. 5
Let us first discuss how the lemmas are generated. The modification of the set of assumptions of the conjectures by using the lemmas will be described in the next part. conjecture coding into terms ¬(ϕ → ¬ψ) ⊢ ϕ t(n(i(A, n(B)))) ⇒ t(A) ¬(ϕ → ¬ψ) ⊢ ψ t(n(i(A, n(B)))) ⇒ t(B) ϕ ⊢ ¬ϕ → ψ t(A) ⇒ t(i(n(A), B)) ψ ⊢ ¬ϕ → ψ t(B) ⇒ t(i(n(A), B)) ¬(ϕ → ϕ) ⊢ ψ t(n(i(A, A))) ⇒ t(B) ⊢ ϕ → (ψ → ϕ) t(i(A, i(B, A))) ϕ → ¬(ψ → ¬χ), ϕ ⊢ χ (t(i(A, n(i(B, n(C))))) ∧ t(A)) ⇒ t(C) ⊢ ϕ → ϕ t(i(A, A)) ⊢ ¬ϕ → (ϕ → ψ) t(i(n(A), i(A, B)))) ⊢ ¬¬ϕ → ϕ t(i(n(n(A)), A)) ⊢ ϕ → ¬¬ϕ t(i(A, n(n(A))) total cost of the conjectures: cost for proving the lemmas: total cost: Let a set of proofs1 P be given. We collect all the clauses that appear in the proofs and that were derived only from the assumptions into a single set
L = [ {c | c is a clause in P derived only from assumptions and without Skolem symbols}
P∈P
We do not include clauses that were derived from the negated conjecture, because they are not true formulas in our theory. Also we remove those clauses that contain Skolem symbols created by the prover, because these symbols have different meaning in different runs of the prover. (In future we might implement the reverse skolemization algorithm [CP80, CP93] to deal with such formulas.)
Thus, the clauses in L don’t contain any skolem symbols, but they have no special form, they can contain arbitrary number of positive and/or negative literals.
Note that although it would be an obvious thing to do, we don’t use the conjectures as lemmas. The reason is that the conjectures are not necessarily clauses, therefore we can’t process them the same way as the clauses produced by the prover. As it turns out, many of the conjectures are then anyway discovered as lemmas by the system. However, this issue deserves a better solution in the future.
From the set L we construct a minimal L′ set with respect to subsumption such that L′ has the following properties: 1. L′ ⊆ L, therefore L′ contains only true formulas.
1Recall that for us a proof is a successful run of the prover that proves a particular conjecture from a given set of assumptions. 2. for every d ∈ L there is c ∈ L′ such that c ⊑ d.
3. for any pair c ∈ L′, d ∈ L′ we know that c doesn’t subsume d: c 6⊑ d.
Therefore, L′ contains just the most general variants of the lemmas appearing in L.
The clauses from L′ are then used as lemmas to modify the set of assumptions of the conjectures.
Now let us have a clause c that is a lemma, c = L1, . . . , Lk, ¬Lk+1, . . . , ¬Ln where Li are atomic formulas. Let |Li| be the number of function symbols appearing in Li. Let P by a proof whose set of assumptions we want to improve by c. We would like to have an estimate that would tell us, if it is likely that c will contribute to the proof P. A natural idea suggests itself that the more often an atomic formula Li occurs in the proof P the more likely the lemma will contribute and also that the longer Li is (measured in the number of symbols) the more likely it will shorten/speed up the proof. Therefore our estimation formula is defined by n weight(c, P) = ∑ |Li| · (the number of occurrences of Li in P) i=1 (1) There are many other possible estimation methods. One may, for example, take into account the number of formulas in the proof which the lemma subsumes, look for similar terms in the lemma and in the proof, etc. 5.2
In order to evaluate the applicability of lemmas, we need to have a criterion for the cost of a proof: Notation 3 (Measure of a proof) A proof measure is a function that maps proofs into nonnegative real numbers.
We use the following proof measures: the number of processed clauses reported by the prover; this measure is closely related to the time the prover spends while searching for the proof of the conjecture, but is independent of the hardware of the computer the prover runs on; the length of the proof is the number of formulas appearing in the proof that is constructed by the prover; the size of the proof is the total number of occurrences of function symbols (not predicate symbols) appearing in the proof that is constructed by the prover.
The length and the size of a proof are also independent on the hardware of the computer being used.
Notation 4 If we are proving a conjecture C from assumptions A1, . . . , An, we denote the measure of the proof by If the prover is not able to conduct the proof we set ||A1, . . . , An
C|| ||A1, . . . , An
C|| = +∞ Remark 1 (The proof size/length) If we could prove all the given conjectures together, the size/length of the resulting hypothetical proof would be of course less than the sum of the sizes/lengths of the individual proofs of the conjectures. But in most cases the prover is not able to prove all the conjectures together, therefore the system proves the conjectures one by one. The system then tries to compact the proofs of the conjectures to make them closer to the size of the hypothetical proof.
The number of generated lemmas is usually very large, so only some of them will be included in the output. Such lemmas are marked as accepted. Each lemma is initially unaccepted. When the system figures out that the lemma is worth including in the output, it marks it as accepted.
For each conjecture or lemma C the system maintains a list SC of sets of assumptions that were used to produce different proofs of the conjecture.
Each such a set S ∈ SC is marked as accepted iff all the lemmas it contains are accepted. The initial set of assumptions of each conjecture contains no lemmas, hence it is always accepted. Now, we may define:
Sbest ∈ SC
C of a conjecture C is an accepted set of assumptions that produces the best proof of C with respect to the proof measure: ∀S : ((S ∈ SC) ∧ (all the lemmas in S are accepted)) ⇒ ||S C|| ≥ ||SCbest
C|| (2) If there are several sets of assumptions that match the criteria for the best accepted set (they produce proofs of the same measure), we arbitrarily choose one among them.
Let us call the proof of C produced from Sbest the best accepted proof of C.
C Remark 2 (System output) The output of the system consists of all the input conjectures and all the accepted lemmas at the time the system finishes execution. For each of these conjectures or lemmas the best accepted set of assumptions is presented. 5.3
The outline of the work of the system is as follows: 1. The system first tries to prove all the given conjectures one by one. Let C be the set of those conjectures that were successfully proved. Let L be the set of constructed lemmas and let La ⊆ L be the set of lemmas that are accepted. Initially, these sets are empty. 2. The system takes the best accepted proofs of all the conjectures and accepted lemmas.
From those proofs the system constructs new lemmas as described in section 5.1. It sets
L = L ∪ {the newly constructed lemmas} 3. The system produces pairs consisting of a best assumption set of a conjecture and of a lemma that will be used to improve the set of assumptions of the best proof of the conjecture. It takes all the new lemmas together with the lemmas it already has constructed before and combines them with all the best accepted sets of assumptions of all the conjectures and accepted lemmas. This way it produces every possible pair of
L × {SCbest |C ∈ C ∪ La} However some pairs of a lemma l and the best set of assumptions SCbest of a conjecture C have to be excluded, namely • if already l ∈ SCbest, or • if the lemma l is the conjecture C itself, or • if the conjecture C is directly or indirectly used to prove l; this means that either C is one of the assumptions in the best accepted set of l, or it is one of the assumptions in the best set of some conjecture that is an assumption of l, and so on.
Otherwise it could happen for example that there would be two equivalent lemmas, one proving another with a one-step proof. 4. These pairs are sorted according to the estimate described in section 5.1. 5. The system subsequently takes these pairs (l Sbest) starting with the one with the highest , C weight: (a) It tries to conduct a new proof of C using SCbest ∪ {l}. The gain of this single improvement is g = ||SCbest
C|| − ||SCbest, l
C|| (b) If g is positive, it means that the lemma l has brought an improvement. The lemma l is then checked, if its total gain to all the conjectures whose set of assumptions were improved by l is larger than the cost of the proof of l. If so, the system sets
La = La ∪ {l} which means that l is marked as accepted.
If l is accepted, we want to incorporate the lemmas that originate from the proof of l as well as the lemmas that originate from the proofs of the conjectures that use l as an assumption. Hence, in such a case the process is restarted from the beginning and the system goes again to point 2. (c) Until there are any unprocessed pairs (l Sbest) the system takes the next pair and , C goes again to 5a. 6. When all the pairs are exhausted and no improvement was made the system outputs the conjectures C, the accepted lemmas La and their best accepted sets of assumptions SCbest, C ∈ C ∪ La, as described above, and halts.
It may happen that as the result of adding l, some of the assumptions in SCbest are not needed any more and do not appear in the proof. In such a case the system omits them and tries to prove the conjecture only using this reduced set of assumptions. If the proof attempt succeeds, it is evaluated the same way as described above. This practice helps to reduce the number of assumptions appearing in the proofs. Without it, the prover would soon become overwhelmed by the number of assumptions and no further improvement would be possible. In the current version of the system this check is not iterated, so the proof conducted from the reduced set of assumptions is not checked again for redundant assumptions. 6
The system is still under development, therefore we don’t have an in-depth statistics of its behavior. However, we have performed tests on different sets of conjectures from different sources and we present a selection of them.
All experiments were run on a Linux machine with Intel® Pentium® 4 CPU 3.4GHz with 2GB of RAM. The conjectures were proved using E prover with resource limits set to 80 seconds, 512MB RAM and 100000 processed clauses.
We have developed an independent server component that lies between the actual system and the automated prover. The component caches all conducted proofs on a hard-disk and if a client requests the server to perform a proof that has already been processed, the server returns the cached version. This greatly speeds up the development of the system, particularly if we rerun the system many times with different settings or with slight modifications on the same set of problems.
For some cases we include a full list of the conjectures and the lemmas, for others we only summarize the results. 6.1
We used several selected TPTP [SS98] problems concerning set theory. These problems originate from [Qua92]. For presentation in this paper we have converted the machine syntax into a more human-readable form. The meaning of the symbols that we use is summarized in Table 2. The conjectures that were proved are shown in Table 3. The table also shows the results obtained when running the system with the proofs being measured by the number of processed clauses. The second column labeled “level” is an inductively defined property defined for both the conjectures and the lemmas. The axioms have level 0. If a conjecture or a lemma is proved just from the axioms, it has level 1. Each lemma or conjecture has its level set to the maximum level of its assumptions plus 1. This can give us an approximation on how complicated the conjecture or the lemma is. The third column labeled || · ||i shows the initial cost of the proof of the conjecture while the fourth column labeled || · || f shows the final cost of the proof of the conjecture when the system terminates. The fifth column shows the actual formula converted into a human-readable form. The last column shows which lemmas were finally used to prove the conjecture.
Some of the conjectures in the listings may have levels greater than 1 although they don’t use any lemmas or the level of a particular conjecture is higher than one plus the level of the lemmas that are used to prove it. The reason is that the user has specified that some other A ⊆ B {A, B} hA, Bi {A} A[1] A[2] A ∈ B A A × B / 0 A ∩ B U member of(A) conjectures should be used as assumptions to prove the conjecture and they increase the level of the conjecture.
We can see that often the conjectures that were harder to prove with respect to the proof measure have a higher level. This means that they were finally proved using several layers of lemmas.
Several conjectures that were too complicated are omitted for brevity.
The lemmas that the system generated with the processed clauses count proof measure are in Table 4. The lemmas are clauses, but for the presentation we have converted them into a more readable form using implication notation. As the lemmas have no initial set of axioms given by the user, they also have no initial cost, so only their final cost is shown.
They are sorted by their total accumulated improvement with respect to the proof measure, the more useful lemmas are at the beginning of the table. This is however only an informative ordering, as it depends very much on the order in which the lemmas were tried. For example, consider some two almost same lemmas l1 and l2. Whichever is chosen second will bring no improvement as the assumption sets were already improved by the one chosen first.
The lemmas are more or less complicated formulas that the system found useful for proving the conjectures. This can give us an interesting comparison, as the input conjectures were selected by a human, whereas the lemmas were constructed by a machine. Tables 5 and 6 show the results on the same set of conjectures when different proof measures were selected. Many of the lemmas appear in all three tables, although in different positions. Such lemmas seem to be essential for the automated prover when working with this particular theory.
Note that some of the lemmas the system has found are just conjectures reformulated as clauses. In such a case the system usually proves such conjecture using the lemma in a single step and then further improves the proof of the lemma.
Table 7 shows the summary of achieved results. For each proof measure the initial and the final cost of the proofs is shown. C31 C32 C33 C34 C35 ((AA ∈⊆ U{B),∧CA})=∧ B(C⇒∈ A()A∧∈(B{B∈,CA}))⇒ A = {B,C} lemmas L7 L6 L7 L7 L13 L5 L8 L9 no. level L1 2 L2 1 L3 3 L4 4 L5 1 L6 1 L7 1 L8 1 L9 1 L10 2 L11 1 L12 1 L13 1 L1 L1 L2 L4 L2 L9 L1 L10 lemmas L2 L1 L2 L5 6.2
These theorems address basic boolean properties of sets in the Mizar database for mathematics. The conjectures were converted from the Mizar language by Josef Urban [Urb04, Urb03] into a form suitable for automated theorem provers.
The system was rather effective for reducing the number of processed clauses required to prove these set of conjectures. Table 8 shows the summary of achieved results. For each proof measure the initial and the final cost of the proofs is shown.
In this section we give detailed results for the example in section 4. The formulas are presented using standard logic symbols.
Table 9 shows the conjectures along with the results obtained when running the system with the proofs being measured by the number of processed clauses and Table 10 shows the lemmas that were found.
no. level C1 8 C2 11 C3 7 C4 2 C5 9 C6 8 C7 5 C8 3 C9 11 C10 7 C11 12
Because we code propositional formulas into terms of predicate logic, we can express much more than just that a propositional formula is a theorem. We can also express meta-theorems that speak about provability of different formulas and what are the relations between them. For example, recall how that modus ponens rule was coded as (t(A) ∧t(i(A, B))) ⇒ t(B). The system derived many lemmas of similar nature, thus discovering many admissible rules. This fact becomes much more interesting in the case of modal logic, described in the next section, where the deduction theorem does not hold, hence the admissible rules have much greater importance. no. level L1 6 L2 6 L3 3 L4 1 L5 3 L6 8 L7 7 L8 8 L9 5 L10 8 L11 8 L12 1 L13 6 L14 5 L15 10 L16 2 L17 5 L18 2 L19 4 L20 6 L21 11 L22 6 L23 2 L24 6 L25 3 L26 3 L27 7 L28 1 L29 7 L30 6 L31 4 L32 6 L33 9 L18 L12 L27 L12 L12 L18 L4 L19 L7 L4 L7 L12 L9 L12 L4 L2 L18 L31 L17 L31 L12 L15 L9 L18 L4 L12 L12 L23 L12 L18 L4 L32 L9 L18 L25 L12 L17 L31 L9 L13 L11
proof measure number of processed clauses proof size proof length S5 modal logic uses meta-theorems (mentioned above), since the theorem of deduction doesn’t hold in S5. From this point of view S5 is an interesting example.
This set of conjectures is similar to the previous example. We have used [Hal05] to construct an axiomatization for S5 modal logic with the three Hilbert’s axioms for propositional logic, axioms K, T and 5 and modus ponens and necessitation rule. We have used the same formula coding with an additional unary function symbol l(. . .) for the modal operator 2. proof cost no. of accepted lemmas 120000 100000 80000 60000 40000 20000 0 0 45 40 35 30 25 20 15 10 5
For this example we also show a graph that illustrates performance of the system, see Figure 1. The x axis shows time points distinguished by the total number of lemmas (both accepted and unaccepted) the system has used at least in one proof. The thick line shows how the total cost of the proofs evolved and corresponds to the tick marks on the left. The thin line shows the number of lemmas that were marked as accepted and corresponds to the tick marks on the right. As we can see, the cost of the proofs was reduced to about 1/3 with the first 10 lemmas. The cost of the proofs then gradually decreased and the lemmas that were accepted often brought only a slight gain. There were two more significant improvements at the points 40, 81 and 97, when interesting lemmas were discovered and sudden advancements were made.
Most of the the lemmas that were discovered say that a particular proposition is a theorem of S5. But the system also discovered several lemmas that describe admissible rules of S5. For example the lemma L40 in Table 15 states that from 2B and B → A we can derive 2A.
Table 16 shows the summary of achieved results. For each proof measure the initial and the final cost of the proofs is shown. formula ⊢ (A → A) ⊢ (2P → P) ⊢ (A → ¬¬A) ⊢ A ∨ ¬2A ⊢ ¬A ∨ 2A ⊢ (¬¬A → A) ⊢ ((¬A → A) → A) ⊢ (¬A → (A → B)) ⊢ 2(A → ¬2¬A) ⊢ (P → 2¬2¬P) ¬(A → A) ⊢ B A ⊢ (¬A → B) B ⊢ (¬A → B) ¬(A → ¬B) ⊢ B ¬(A → ¬B) ⊢ A ⊢ ((A → B) → (¬B → ¬A)) ⊢ (A → (¬B → ¬(A → B))) A, B ⊢ ¬(A → ¬B) ⊢ 2(¬2¬P → 2¬2¬P) ¬(B → ¬A) ⊢ ¬(A → ¬B) 2(A → B),2(B → A) ⊢ 2(2A → 2B) ¬(A → ¬¬(B → ¬C)) ⊢ ¬(¬(A → ¬B) → ¬C) L43 L25 L37 L2 L36 L33 L17 L2 L1 L19 L10 L19 L14 L20 L23 L28 L2 L13 L22 L1 L42 L9 L24
L20 L23 L14 formula (A → C), (A → (C → B)) ⊢ (A → B) (A → C), (C → B) ⊢ (A → B) C, (A → (C → B)) ⊢ (A → B) 22B, (B → A) ⊢ 2A ⊢ (¬¬A → A) (¬B → A) ⊢ (¬A → B) (A → (¬C → ¬B)) ⊢ (A → (B → C)) (¬A → ¬B), B ⊢ A formula (A → C), (A → (C → B)) ⊢ (A → B) (A → C), (C → B) ⊢ (A → B) C, (A → (C → B)) ⊢ (A → B) (¬B → A) ⊢ (¬A → B) ⊢ (¬¬A → A) 22B, (B → A) ⊢ 2A (¬B → ¬A) ⊢ (A → B) lemmas L4 L1 L1 L3 L2 lemmas L1 L7 L24 L43 L13 L8 L25 L1 L15 L3 L31 L1 L2 L32 L10 L32 L15 L10 L10 L1 L20 L6 L11 L32 L19 L1 L37 L15 L19 L2 L1 L29 L24 L28 L2 L29 L10 L9 L43 L2 L29 L32 L1 L15 L29 L25 L17 L33 L1 L7 L9 L25 L1 L43 L17 L29 L33 L2 L24
proof measure number of processed clauses proof size proof length
The system again performed very well in the case when the measure was the number of processed clauses. This time, the total cost of the proofs was reduced to less than 2%. 7
As the system is particularly efficient in speeding up the prover, we believe that it could be modified to search for lemmas that would make it possible to prove conjectures that the prover alone wasn’t able to prove. This will require a change of strategy, because currently the system looks primarily for lemmas that improve already existing proofs of the conjectures and therefore are not general enough to prove some new unknown conjecture.
We would also like to investigate the nature of the lemmas that help to improve particular proof measures in order to develop a better strategy for their evaluation.
Finally, we plan to perform a in-depth testing of the system on various sets of conjectures from different sources. 8
Given a related set of conjectures, it is possible to automatically construct lemmas that can significantly reduce the cost of the proofs of the conjectures. The results are summarized in Table 17 for convenience.
set of conjectures TPTP set theory Mizar set properties Meredith’s axiomatization S5 modal logic
The system that we have developed performs well on different sets of conjectures, particularly if the cost of the proofs of the conjectures is measured in the number of clauses processed by the prover. The system can also improve the size and/or the length of the proofs, although it is not as effective in these cases. [AS92]
Owen L. Astrachan and Mark E. Stickel. Caching and lemmaizing in model elimination theorem provers. In Deepak Kapur, editor, CADE, volume 607 of Lecture Notes in Computer Science, pages 224–238. Springer, 1992.
Simon Colton. Automated Theory Formation in Pure Mathematics. Distinguished
Dissertations.