Experimenting with Machine Learning in
Automatic Theorem Proving∗
Josef Urban†
January 8, 1999

Abstract
First the notion of the heuristic and its importance for automatic theorem proving is explained. The question of how to construct a useful systemof heuristics and notions is posed, and it is argued for the importance oflearning. A simple example of learning a lemma is shown using the Inductive Logic Programming system Progol.
Second a general framework for learning heuristics is discussed and theproof checking system Mizar providing a large body of mathematics isfound suitable to learn upon. The process of modifying Mizar for use with
Progol is shortly described, e.g. turning the mathematical texts to Prolog
structures, creating initial notions, creating the initial base of rules fromtheorems and deﬁnitions, preparing proofs for learning, and problems withpolymorphism.
Finally ﬁrst experiments in this environment are described, which include learning the notion of atomic formula and learning how to use initialrules in the proof of Rolle’s theorem.

∗

This work was supported by Esprit Project 20237 Inductive Logic Programming II
This article is an abridged version of the master thesis done under the guidence of doc.
RNDr. Petr Štěpánek, DrSc. at the Faculty of Mathematics and Physics of the Charles
University
†

1

1

Automatic Theorem Proving and Heuristics

This section should shortly explain the notion of heuristic, its importance for
automatic theorem proving (ATP), and it is the motivation for the work describedin next sections.
It is well known, that one of the main problems of ATP algorithms is their computational complexity ( also combinatorial explosion ). In resolution based theorem provers this happens when the empty clause is not derived quickly enoughand the prover keeps generating new clauses over and over, until the amount ofpossible resolutions is intractable.
There are various methods how to guide resolution steps (e.g. which clausesshould be taken to be resolved upon), generally called uniform proof procedures( see [Chang and Lee 73] ), because they can be used for proving theorems inany axiomatic theory without any domain speciﬁc knowledge. Many people (e.g. [Bundy 83] ) think that provers based only on resolution are insuﬃcient forproving theorems in more complex areas ( e.g. calculus ).
One of the methods which try to cope with such problems is looking at theway people solve them and trying to implement human methods in AI algorithms. An example of using this method is Lenat’s Artiﬁcial Mathematician
described in [Lenat 78], where system of heuristics derived from human behavior
does mathematical explorations.
Similarly, we can look at the way people prove theorems and try to extract
some heuristics for use in ATP. Here by heuristic we mean some rule, method orexperience which tells us what to do in some situation, it does not need to be
perfectly true . . . e.g. it suﬃces that it often helps us, and it does not need to beprecisely formulated in some well deﬁned notions, on the contrary, it often uses
vague notions (e.g. ’similarity’ ).
Some examples of heuristics used in mathematics are:in Logic: ’Proving something for all formulas is often done by induction on
the complexity of formula’in Calculus: ’It has usually little sense to think about the inner structure of areal number as a set’in Set Theory: ’Try some diagonalization’The system of heuristics we use is probably quite complicated, e.g. sometimes wetry to prove something using some method, then we see it is a road to nowhere
and think why the previous method failed, and on the basis of it try anothermethod. So we have not only heuristics formulated in the language of its domain
theory, but also heuristics formulated by means of other heuristics and results of
their application, e.g.
2’There is no sense in applying some rule ’R’ and immediately after it applying
the rule inverse to ’R’ ’
or’Try substituting ǫ for δ, and if the result is 2ǫ, try substituting ǫ/2’
In my opinion, the quality of a theorem prover depends immediately on the setof heuristics that its authors recognize, and on the way they link them together
and add to some standard proving techniques such as resolution. So it seems weshould be interested in the question how to ﬁnd heuristics, and more generally
a suﬃciently large system of heuristics, that would give us recommendations fortheorem proving similar to those of human.

2

Finding Heuristics, Learning

The most straightforward way of creating heuristics seems to be simply thinkingof them and typing them in. It corresponds to teaching done completely byexplanation, i.e. we have to provide deﬁnition for every notion our heuristics use,deﬁne many relations among heuristics, and worse of all, try to ﬁnd them all on
all levels ( e.g. heuristics about using heuristics, etc. ).
There is probably some redundancy in this method, because there surely aresome heuristics about ﬁnding heuristics, so why not let them ﬁnd the rest for
us. I think ’learning from examples’ could be a (meta)heuristic of this kind andin this work experiments are carried out to ﬁnd out what is possible to discoverusing this heuristic.
The reason for trying this heuristic comes again from comparison with humans. When we learn mathematics, it often has the form of watching sometheory being developed, i.e. watching some necessary notions being deﬁned, theorems about them being proved and maybe some interesting examples of applying
the theory being shown. In this framework there is often very little said about
the motivation for deﬁning exactly the notions deﬁned, and leading the proofs oftheorems exactly the way it was done. Yet after some time we are able to produce
some proofs ourselves or deﬁne and explore interesting notions ourselves, we not
only remember what was shown to us, but also know heuristics telling us whether
something is interesting or not and what to do when we want to prove something.
In my opinion this is ( at least partly ) caused by our ability to generalise
what we are shown to some useful heuristics or vague notions in which we actually
think. This generalisation happens often quite spontaneously, e.g. many people
when ﬁrstly shown the notion of continuous real function would guess it would
also mean diﬀerentiability, or when shown several proofs in calculus and grouptheory they would be able to speak about the most striking diﬀerences between
3the two theories.
So in order to gain some heuristics, we would like to simulate this processof generalising examples in computer. There are various approaches to the taskof machine learning and many systems implementing them, the most convenient
for the speciﬁc task of learning heuristics seemed to me to be the Progol system[Muggleton 95, Roberts 97] coming from the ﬁeld of Inductive Logic Programming.

3

Progol, Simple Example of Learning a Rulefrom Examples of Its Use

3.1

ProgolProgol is a Prolog interpreter enhanced by predicates that enable learning. Progoltries to generalise examples given to it to some Prolog clauses whose form wedetermine by special mode predicates, so the method implemented here is called
Mode-Directed Inverse Entailment.
The quickest way of showing how to learn something using Progol is probably
running through some example, here the example of learning classiﬁcation ofanimals which is distributed together with Progol is chosen.
In this example we want to learn deﬁnitions of animal classes such as mammals or birds, from some positive examples such asclass(eagle,bird). class(bat,mammal). class(dog,mammal).
and some background knowledge such as
has legs(eagle,2). has legs(bat,2). has legs(dog,4). has milk(bat). has milk(dog).

So we want to learn clauses of the form e.g. class(A,mammal):- has milk(A). We specify the required form of output clauses by predicates modeh/2 andmodeb/2, where we determine which predicates can occur in the head and in the
body of output clauses. Here these declarations would look something like:-modeh(1,class(+animal,#class))?
:-modeb(1,has legs(+animal,#nat))?
:-modeb(1,has milk(+animal))?
The ﬁrst clause says that the output clause should have predicate class/2 in
its head with ﬁrst term being a variable of type animal and the second term
being a constant of type class. The two following clauses say that in the body we4allow one occurence of the predicate has legs/2 and one occurence of the predicate has milk/1. The types used in these declarations have to be deﬁned, here it
would be e.g.
animal(eagle). animal(bat). animal(dog). class(bird). class(mammal).
The synbol ′ +′ in the mode declarations speciﬁes we want the term to be a variable ( exactly an input variable), while the symbol ′ #′ means we want the term
to be a constant. The third possibility is ′ −′ , which represents output variable.
We should also set some parameters inﬂuencing the learning process (e.g. howcomplex hypotheses Progol creates ). If everything goes well, Progol really generalizes our examples and produces clauses likeclass(A,mammal):-has milk(A).

3.2

Simple Example of Learning a Rule from Examples of
Its UseThe ﬁrst thing we would like to know when thinking about ﬁnding heuristics orinteresting notions by machine learning is whether it is possible at all, at least insome simple case.
In the ﬁrst experiment, a simple lemma (exactly a deﬁnition) sub(x,y)=x+(-y)
was learned from examples where this lemma was used and some counterexamples. Here the simpliﬁcation is that
• we know beforehand what we learn and can supply additional examples
or counterexamples as well as adjust parameters for learning to obtain theright result• the learned lemma is not a heuristic deﬁned in possibly vague notions, we
can constrain the search to mathematical expressions• the background knowledge used in the learning did not go too much indetail, thus the learned clauses would have some drawbacks.
The positive examples for this learning were produced using the IMPS (Interactive Mathematical Proving System). Several mathematical expressions containing
the term sub(. . .,. . .) (e.g. sub(x∗ z, z ∗ x) = 0 ) were typed in and IMPS rewrote
them using our lemma, so the rewritten expressions would instead of the termsub(. . .,. . .) contain terms like (. . .)+(-(. . .)) (e.g. (x ∗ z) + (−(z ∗ x)) = 0 ).
The pairs [expression bef ore rewriting, expression af ter rewriting] were given
to Progol as examples of the predicate similar/2 and some counterexamples were5

added. We would like Progol to ﬁnd what all these examples have in common.
That’s why the predicate gener/2 was deﬁned, where gener(A,B) should standfor ’A unifies (in the sense of IMPS) with some term in B’. Following previous
example,gener(sub(x, y), sub(x ∗ z, z ∗ x) = 0)
would be true, because sub(x, y) uniﬁes with the term sub(x ∗ z, z ∗ x) 1 . Given
these examples and deﬁnitions, we can use mode declarations to specify the exact
form of the clause searched for:modeh(1,similar(+expr,+expr))?
modeb(2,gener(#expr,+expr))?
This says in the head there should be something like similar(A,B), while in the
body we allow two occurences of the predicate gener/2 each of them having a
constant term as a ﬁrst argument. What we hope for is that the outcome will be
the clausesimilar(A, B) : −gener(sub(x, y), A), gener(x + (−y), B).
which means in all examples the expression before rewriting contains a term generalised by sub(x, y) and the exprression after rewriting contains a term generalised by x + (−y), and in which the learned lemma is already apparent.
Of course, we could impose some stronger conditions, e.g. we could requirein each pair that the generalisation in both expressions occurs at the same position. I think it is not necessary, because when there is a lot of examples andcounterexamples then there is a good chance that the wrong hypotheses will not
succeed in generalising them.
The real simpliﬁcation that took place in deﬁning predicate gener/2 was that
only one ’generalising variable’ (e.g. ’x’) was allowed. You can genaralise any
term by a variable, but when learning, this variable will always be ’x’. I think it
would be possible to correct this drawback, but it would be necessary to remember
somehow that ’x’ is already bound to some term, and always check whether a
new term is already generalised by some variable.
So the clause Progol actually learned diﬀers from above in that instead of two
variables ’x’,’y’, it contains only one variable ’x’:
similar(A, B) : −gener(sub(x, x), A), gener(x + (−x), B).
This is what it really looks like when the λ-calculus notation of IMPS turned tolists is used:1
The notation here is simpliﬁed in that IMPS uses λ-calculus and IMPS expressions wereturned to lists for use in Progol.

6

similar(A,B) :gener([[apply-operator,[sub,[rr,rr,rr]],[x,rr],[x,rr]],rr],A),
gener([[apply-operator,[[lambda,[[rr,x,y]],[[apply-operator,[+,[rr,rr,rr]],[[apply-operator,[-,[rr,rr]],[y,rr]],rr],[x,rr]],rr]],[rr,rr,rr]],[x,rr],[x,rr]],rr],B).
This learning used ﬁve examples and two counterexamples and took about 4
seconds on P133.

4

A Framework for Larger Experiments

In my opinion the previous example shows that in principle it is possible to ﬁnd
in mathematical texts some knowledge that is not explicitly presented there, it
is implicit or hidden ( . . . sort of kabbalah ).
Finding some nontrivial and useful heuristics in some larger text is certainly
going to be harder, because• we will have to learn how to choose from a larger text some parts thatare suspect to have something in common ( so that we could do some
generalisation on them )• the heuristics we know use a language that diﬀers from that of mathematics,
e.g. it contains notions like similarity, inverse rule, induction, triviality,
heuristic, integral, theorem of calculus, etc, and in the beginning, we do
not know deﬁnitions of these notions.
I think that the two problems of ﬁnding heuristics and ﬁnding notions thatheuristics use should be solved in the same time. It may happen, that someconditions will occur quite often in the deﬁnitions of the heuristics found so far,e.g. it may turn out that some group of lemmas is used to some expression only
when it contains some typical functions or predicates. We can then give somename to this kind of expression, e.g. ’integral’, or ’expression of set theory’, store
their deﬁnition in lower notions somewhere ( e.g. ’predicate symbols(X,[ǫ])’ for
X being an ’expression of set theory’ ), and use them for ﬁnding more complex
heuristics.
So when we want to try ﬁnding heuristics and their language, we should have• some mathematical texts, where we will search for the heuristics and theirnotions• some basic notions that describe these texts (e.g. knowing that ′ ǫ′ is apredicate symbol comes in handy )• some system that should enable us to choose and prepare parts of themathematical texts for learning7• a learning system . . . here it is Progol
So far we often used comparison with human thinking as a method telling us
what to do next. If we want to continue using this method, the mathematicaltexts we learn upon should be as similar to human textbooks as possible. On theother hand, a genuine textbooks already contain great deal of natural language
and vague notions and it would be hard even to construct some set of initialnotions describing the structure of the texts (e.g. telling the computer what is atheorem or proof or even a correct proof).
It follows that we are looking for mathematical texts that are formalised insome way, but at the same time they are as close to human mathematics as
possible. I ﬁnally chose the MIZAR system, which will be now shortly described.

5

The MIZAR system

The MIZAR system [Rudnicky 92] is an outcome of a project started in Poland
in 1973. In this project a syntax for writing mathematical articles was developed
and many articles were written using this syntax. The syntax was created tocomply with two major requirements:• it should make computer checking of the correctness of articles possible• it should resemble human mathematics as much as possible, thus making
it easier for the mathematicians to write their articles in this form
So the distribution of the MIZAR system (found on internet) consists of twoparts, the system checking the correctness of newly written articles and about
500 articles from various ﬁelds of mathematics that were already checked andapproved to be in the distribution. The articles not only have some informativevalue, they also enable us to use notions deﬁned or theorems proved in them,thus making writing new articles in more complex ﬁelds quite easy.
Here some parts of the article about sets are shown::: Some Basic Properties of Sets:: by Czes{\l}aw Byli\’nski
environvocabulary BOOLE,FAM_OP;
theorems TARSKI,BOOLE,ENUMSET1;
begin
reserve v,x,x1,x2,y,y1,y2,z for Any;Th12:{x} c= X iff x ∈ X
proof

8

thus {x} c= X implies x ∈ X
proof x ∈ {x} by TARSKI:def 1; hence thesis; end;
assumeA1: x ∈ X;
let y;
thus thesis by A1,TARSKI:def 1;
end;
definition let X1,X2;
func [: X1,X2 :] means:Def1: z ∈ it iff ex x,y st x ∈ X1 & y ∈ X2 & z = [x,y];....

Articles consist of keywords, e.g. environ, reserve, theorem, proof, definition,
thus, hence , comments, initial declarations ( names of articles we will referto), reservation of variables for certain types ( here the type Any means set ),theorems, deﬁnitions, schemes and auxiliary items. Auxiliary items often havethe same form as theorems, Th12 is of this kind, it is some lemma with proof.
The deﬁnition shown is the beginning of the deﬁnition of cartesian product, after
the deﬁning formula there should be some proofs of correctness of this deﬁnition.
The structure of schemes is similar to that of theorems, but they usually containsome quantiﬁcation of a predicate or function of some type.
The meaning of keywords is quite similar to their meaning in English and thesyntax allows us to write the proofs in quite a common way, e.g. it is possible
to prove some part by contradiction or to introduce in the course of proof somelemma and give a proof of it. Each article can deﬁne its own notation, so one
symbol can have diﬀerent meanings in diﬀerrent articles, and even in one article
a symbol can have diﬀerent meanings, e.g. when it is a function or predicate
deﬁned in a diﬀerrent way for various types.

6

Preparing MIZAR for Learning

It was necessary for the task of learning to make MIZAR articles at least to
some extent understandable for Progol. Firstly some initial notions describing
the articles were created and then some more complicated predicates were written
and initial base of rules created, which made proof analysis possible.

6.1

Creating Initial Notions, Turning MIZAR Texts to
Prolog Structures

Here the syntax of the MIZAR language in deﬁnite clauses found on the home
page of the MIZAR project was of great help. Deﬁnite clauses such as
9

Atomic-Formula-Expression =Term-Expression-List Predicate-Symbol Term-Expression-List

were turned to Prolog predicates about recursive lists such as
atomic formula expression([A,B,C]) :term expression list(A), predicate symbol(B), term expression list(C).

Similar predicates working basically on the principle of diﬀerential lists wereused for parsing the linear text of articles to recursive lists, e.g. here it would
look likeatomic formula expression(V0,V,[A,B,C]) :term expression list(V0,V1,A), predicate symbol(V1,V2,B), term expression list(V2,V,C).

In fact, this process was quite complicated, because using only the method of
diﬀerential lists would often be very ineﬃcient and parsing the terms and formulas requires some additional knowledge (e.g. priorities of symbols), that can befor each article diﬀerent.

6.2

Problems with Polymorphism

In MIZAR there are many types, and many functions and predicates have diﬀerent deﬁnitions for diﬀerent types, and sometimes it is quite complicated to tellexactly which deﬁnition was used (e.g. function deﬁned for some type may be
used to a more special type, however when deﬁnition for the more special type
exists, it should be used, etc ).
This seemes to be quite unsuitable for some possible learning in Progol, because only to be sure we understand some term or formula correctly, we would
have to include all that polymorphism resolving machinery in the backgroundknowledge, slowing down the actual learning.
So an attempt was made to get rid of the polymorphism, basically by numbering all diﬀerent meanings of functions, predicates and types, and preprocessing
the articles with a program which tries to guess the right meanings and adds thecorresponding numbers to symbols for functions, predicates and types.

6.3

Creating Initial Rules

If we want to analyse proofs, we should be able to apply some lemma or theorem
in some proof situation. That is why applicable rules were constructed from thetheorems, deﬁnitions and schemes in MIZAR articles.
10It is easy to create a rule from a theorem of the form ’A implies B’. It already is a rule, applicable in case we want to prove an instance of ’B’, changing
it to an instance of ’A’. More generally, when we want to prove a disjunction
WW{A1 , . . . , An } and we know that disjunction {B1 , . . . , Bm } is true, the algorithm is:
1. ﬁnd the intersection2 {C1 , . . . , Cl } = {A1 , . . . , An } ∩ {B1 , . . . , Bm }2. if this intersection is empty, thenW

{B1 , . . . , Bm } is not applicableW

3. else let {D1 , . . . , Dm−l } = {B1 , . . . , Bm }\{C1, . . . , Cl } , the proof of {A1 , . . . , An }V
is reduced to the proof of {¬D1 , . . . , ¬Dm−l }W

for if none of Di is true, some Cj must hold ( because {B1 , . . . , Bm } is true)Wand consequently {A1 , . . . , An } holds.
So theorems from MIZAR articles were converted to conjunction of disjunctions, and each disjunction was taken to be an initial rule ( it means usually morethan one rule were created from a theorem). Basically the same was done with
schemes and deﬁnitions, deﬁnitions ﬁrst being turned to equivalences.
The problem here arises if existential quantiﬁcation is present in some theorem, scheme or deﬁnition. MIZAR does not require some skolemization, in thecourse of proof special ’reasoning items’ are used to handle existential quantiﬁcation. That is why the parts of formulas beginning with existential quantiﬁer wereleft intact, and the plan is to use similar reasoning items for their eliminating as
MIZAR does.

6.4

Preparing Proofs for Learning

The MIZAR proofs consist of various reasoning items. These items in most cases
modify the thesis. At the start of a proof the thesis is simply the theorem being
proved, and the proof is ﬁnished when there is nothing else to prove, i.e. thethesis is empty.
The problem is, that the current thesis is apparent only at the beginning andat the end of the proof, and if we would like to know the thesis somewhere in
the middle of the proof, we would have to run through all reasoning items fromthe beginning to that point and apply them. It is quite inconvenient, because
we could want to learn e.g. why exactly some reasoning item was used at somepoint of the proof, and for such learning knowing the form of the thesis at thatpoint is essential.
That is why a program which determines the thesis was written. Proofs are
before learning preprocessed with this program, and it usually adds the current
thesis to reasoning items and also numbers the reasoning items in a uniform way,
to facilitate orientation in the proof.
2

more exactly: intersection up to an uniﬁcation; this applies also to step 3.

11

7First Experiments with Learning

7.1

Learning the Notion of Atomic FormulaThis experiment was done to try, whether under very favourable conditions it ispossible at all to learn some useful notion. It was carried out in an early stage ofpreparing MIZAR texts for use with Progol, also with the purpose to get feedback
for further modiﬁcation of MIZAR texts.
For this learning, the notion of ’atomic formula’ was chosen, and the task wasto learn this notion using some other initial notions (e.g. ’term’, ’identifier’, etc)
and some examples of this notion. The simpliﬁcation here was:
• We know beforehand the notion we learn, only examples of this notion were
supplied ( together with some counterexamples)• About 100 initial notions describing the texts were created from the MIZAR
syntax. It would be intractable to allow them all in the learning. On theother hand, we have no heuristics yet, that could do the task of choosing themost ’suspect’ initial notions, that should be allowed in the learning. That
is why I chose 8 ’suspect’ initial notions myself, and of course, among them
there were also the notions necessary for the deﬁnition of ’atomic formula’(i.e. term list and predicate)
The examples of atomic formulas were created by choosing all atomic formulas in
the proof of Rolle’s theorem. There were about sixty of them, one counterexample
was added. In this early stage of modifying MIZAR articles, diﬀerential lists wereused instead of recursive lists, i.e. an example of atomic formula would look likef_e([f1,’.’,x,’=’,f2,’.’,x,’+’,r],[])
where f e/2 stands for formula expression (although it should be atomic formulaexpression), and f e(A,B) means ’append(C,B,A) holds, and C is an atomic formula’. In all these examples the second argument was the empty list, so thewhole ﬁrst argument is the atomic formula.
We want to learn the deﬁnition of the predicate f e/2, therefore the headmode declaration is:-modeh(1,f_e(+list,[]))?
The diﬀerential lists are quite unsuitable for working with recursive things such as
formulas or terms ( it is very ineﬃcient), on the other hand here this formalisation
makes writing the body mode declarations quite easy. here they have the form:-modeb(3,term_expression(+list,-list))?
:-modeb(3,identifier(+list,-list))?
:-modeb(3,predicate_symbol(+list,-list))?
....
12

It means Progol will construct hypotheses such asf e(A, []) : −term expression(A, B), identif ier(A, B), predicate symbol(B, C).
and it already is the kind of deﬁnition we are looking for.
The number 3 in the body mode declarations is quite arbitrary, it says thatthe output clause should not contain more than three occurences of each of thispredicates. The more occurences we allow, the more complex will the search be,so it is an attempt to balance the speed of the search with its generality.
The ﬁnal learning used about 60 positive examples and 1 counterexample,
and on PC486/100MHz took (depending on parameter settings) from 50 to 100
seconds. It is very much, mainly because handling terms and formulas as diﬀerrential lists was ineﬃcient. All examples were generalised by the clausef_e(A,[]):- term_expression(A,B), predicate(B,C), term_expression(C,D).

7.2

Learning How to Use Initial Rules in the Proof of
Rolle’s Theorem

One particular approach to learning heuristics is to learn on various proof situations ( described by the formula being proved, the special symbols in it, thetheory to which the formula belongs, etc.), the set of possible solutions of thesesituations (i.e. the initial rules applicable to the formula being proved, or moregenarally the heuristics applicable to the proof situation) and the solution actuallyused in the proof.
To put it more concretly, we could create from the MIZAR proofs triples(1) [proof situation, its possible solutions, the solution actually used in the proof]
and try to generalise them.
In this setting, some of the heuristics already mentioned could be (at leastin principle) learnable, e.g. we could ﬁnd out that if the proof situation has
attributes ’model theory’ and ’st. is being proved for the set of all formulas’, then’induction on the complexity of formula’ is always in the set of possible solutions
and quite often it is also the solution actually used in the proof.
For the ﬁrst learning in this setting, the situation was simpliﬁed in that• as the set of possible solutions only the initial rules applicable to the formulawere taken (we do not know any higher heuristics yet)• the description of proof situation was ommited. It means the examples forlearning will be only pairs(2) [applicable initial rules,the rule actually used in the proof]13

In fact, the set of applicable rules describes the proof situation to someextent, so the ﬁrst two members in the triples (1) are in a simple way
described by the ﬁrst member in the pairs (2).
The examples for this learning were obtained from the proof of Rolle’s theorem ( theorem ’Th1’ in the MIZAR article ’rolle.miz’ ). The reasoning itemsof this proof (there are hundreds of them) were ﬁrst preprocessed in the way
described in (6.4.), and from them only the items that have the form of selfcontained statements were chosen. Examples of such statements are
A0: p ≤ g by Z0;
A01: ].p,g.[ is open by RCOMP 1:25,Z0;r/(n+2)<r by SQUARE 1:14;
C9: rng (h1+c) c= N1 proof ... end;
These items can be divided into three groups:• items with a longer proof beginning with the keyword ’proof ’ and ended
with the keyword ’end’ . . . the item C9 above• items with a ’simple justification’ ( it is a list of references to other items,
theorems, schemes or deﬁnitions, from which the current item immediatelly
follows), that contain a reference to some other item in this proof . . . items
A0 and A01 above . . . they contain reference to the item Z0, which is someassumption made previously in the proof• items with a ’simple justification’ that contain only references to other theorems, schemes or deﬁnitions . . . the third item from above . . . contains
reference to theorem 14 in the article ’SQUARE 1.miz’
The simplest possibility was to choose only the third group for learning, wherestill remains 54 items. Thus we may take into account only the theorems, schemes
and deﬁnitions previously proved, while if we wanted to use also the items fromthe ﬁrst and second group, we would have to consider also references to otheritems or assumptions made in the proof, and the learning would have to be more
complicated.
There are 55 MIZAR theorems, deﬁnitions and schemes used in the proof ofthis theorem (see Appendix A), and from them 90 initial rules were constructed.
For the learning only these 90 rules were allowed. Other possibility is e.g. toallow all rules constructed or to allow all rules from the articles declared in theenvironment declarations of the article ’rolle.miz’. But with both these possibilities the learning would take very long time, because there are about 7000 initialrules ( made from about 60 articles that were necessary for the article ’rolle.miz’) and there are still thousands of rules in articles directly referenced in ’rolle.miz’.
14

To create examples for learning, it was necessary for each of the 54 chosen
items to determine the set of applicable rules. It was done using the program
described in 6.3. The statistics of the results is in Appendix B ( this is no learningyet). In this statistics, two things should be noticed and explained:• Sometimes according to the original proof some rule should be used, but
my program for rule application said the rule was not applicable. This is
usually caused by the incompletness of the program for rule application(e.g. the existential quantiﬁers are not handled properly yet).
• The number of possible applications of some rules is very high (thousands).
It happened because the rules of the form ’a=b’ were also allowed to be
used for rewriting the left hand side to the right hand side of the equationand vice versa. In case one side of the equation is a variable, it uniﬁes withalmost anything, and the rule is applicable many times in diﬀerent ways.
Besides this statistics, the main result of running the program determining theapplicability of rules, are the 54 pairs [list of applicable rules, the rule actuallyused in the proof] ( one for each of the chosen reasoning items). For example, thepair[[RCOMP_1:15,SQUARE:14,BOOLE:def8],RCOMP_1:15]

means that to prove one of the 54 reasoning items the theorem RCOMP 1:15
was used, but theorem SQUARE:14 and deﬁnition BOOLE:def8 were also applicable.
In addition to these 54 positive examples, about 400 counterexamples werecreated, taking the 54 lists of applicable rules ( the left hand sides of the pairs)
and for each list, all its members (except those in the positive examples) weretaken as a right hand side of the counterexample pairs. It means for the example
above we would create two counterexamples[[RCOMP_1:15,SQUARE:14,BOOLE:def8],SQUARE:14][[RCOMP_1:15,SQUARE:14,BOOLE:def8],BOOLE:def8]

In this ﬁrst experiment, positive examples ( denoted e.g. by predicate choose/2)
were generalised using the predicates p element/2, n p element/2 which have forthe initial rules the same meaning as member/2, not member/2. Two learnings
were carried out, in the ﬁrst one the posistive and negative examples were as already described, while in the second one the positive and negative examples were
exchanged (i.e. there were about 400 positive examples and 54 counterexamples).
In both cases the mode declarations are:-modeh(1,choose(+rule_list,#rule))?
:-modeb(20,p_element(#rule,+rule_list))?
:-modeb(2,n_p_element(#rule,+rule_list))?
15

So we will learn clauses of the formchoose(A,SEQ 4:46) :- p element(A,SEQ 1:def8).

which in the ﬁrst case means:’If both SEQ 4:46, SEQ 1:def8 are applicable, then the rule SEQ 4:46 should be
used’
while in the second case the meaning is:’If both SEQ 4:46, SEQ 1:def8 are applicable, then the rule SEQ 4:46 should not
be used’

7.2.1

Results of This Learning

In the ﬁrst case the learning was quite unsuccesful, while in the second case theresults seem to be quite good. I think the reason is the ratio of positive andnegative examples.
In the ﬁrst case the number of counterexamples was too high to allow good
generalisation (i.e. the closed world assumption used when they were created was
too strong). The 54 positive examples were generalised to 50 clauses, from which
only 18 were newly created deﬁnitions, while the rest were the original examples.
The second case is more interesting, the about 400 positive examples weregeneralised to 140 clauses, only 34 of them were the original examples, while
the rest were newly created deﬁnitions. This learning took about 2,5 hour on
PC486/100MHz.
More than 100 newly created deﬁnitions are of the formchoose(A,REAL_1:33) :- p_element(NAT_1:38,A).
which in this case means that if both these rules are applicable, REAL 1:33 should
not be used. This form of the most of the newly created clauses tempts to thinkof them as of deﬁning something very similar to ordering of the initial rules usedin the proof (e.g. the previous clause would say REAL 1:33 < NAT 1:38). I tried
to analyse a little this “ordering”, to ﬁnd out something about the results of thislearning.
For 24 rules3 of the 55 holds, that there is no “better” rule, which could be(with some generalisation) interpreted as a hint to use these rules whenever they
are applicable. As early as we look at the ﬁrst rule of these 24 . . . AXIOMS:13
3

In Appendix A there is ’+’ before them16

. . . associtivity of ’+’, we realize, that either the learning set was too special or
our interpretation of the results is too general, because using associativity of ’+’whenever it is possible is surely not the right way to prove theorems.
On the other hand, all of the three rules that are atomic formulas and do notcontain predicate ’=’ (i.e. NAT 1:18, NAT 1:21, RFUNCT 2:10) are among thebest 24. I think it corresponds to the fact that atomic formulas not containing’=’ have in proving the meaning of ’facts’, used in the backchaining wheneverpossible ( atomic formulas containing ’=’ can also be used for rewriting, that is
why most of them (7 of 8) are not among the 24).
Another quite expectable fact is that many of the “top 24” contain some
unusual (in relation to other rules) predicate or group of terms (e.g. ’diff(f,x0)’,’f(Y)’, ’is constant on’, ’0≤y-x’, etc.).
On the other side of the scale there are six rules, that according to our interpretation should be used only when no other rule is applicable. They are
FDIFF_1:def8, REAL_1:26, REAL_1:33, SEQ_2:2, SQUARE_1:14, TARSKI:def2

With the exception of REAL 1:24 all of them contain some expresion of theform ’x=. . .’, the ’most applicable’ (according to statistics given in Appendix B)
rule TARSKI:def2 even containing two expressions of the form ’x=y’.
Finally I created for each rule the list of ’better’ rules. Here the 5 cases where
this list was of length 1 (i.e. the ’second best’ rules) were interesting. These pairs( the second best, the better) are:
NAT_1:19
RCOMP_1:11
RCOMP_1:15
REAL:39
REAL_1:53

AXIOMS:13
RCOMP_1:6
BOOLE:8
SEQ_2:6
REAL_1:14

The rules in the ﬁrst pair have nothing in common, those in the second pairboth contain the term ’[.g,s.]’, the rules in the third pair both contain the predicate ’∈’, and the rule BOOLE:8 that contains more general terms at this predicate
is ’better’, in the fourth pair both rules contain the term ’x/y’ and atomic formula
not containing ’=’ is prefered, and in the last pair the rules contain terms x+y,and the rule REAL 1:14 with the more special term ’x+ -y’ is prefered.
With the exception of the ﬁrst pair, the rules in these pairs are somewhat
similar, they contain the same predicate or similar group of terms. It leads tothe conjecture, that rules which are close in the ’ordering’ found, are often close
also syntactically and applicable in similar situations.

8

Conclusions

The purpose of this work is to try to develop a system for ﬁnding useful notions
and heuristics for theorem proving. The method that is tried is to analyse the17mathematical texts of the MIZAR system using the initial notions of MIZAR
syntax, the initial rules created from the MIZAR theorems and deﬁnitions, some
simple theorem proving predicates written in Prolog, and the Inductive Logic
Programming system Progol.
Three Progol learnings were described. The results of the ﬁrst (learning arule from examples of its use) and the second one (learning the notion of atomic
formula) were previously known, they were carried out to check the feasibilityof this approach at least under very favourable conditions. The result of thethird and largest learning (how to use initial rules in the proof of Rolle’s theorem) is a compression of about 400 examples taken from the proof to 140 clauses,
which when viewed as deﬁning ordering of the initial rules give already somemeaningful heuristics, e.g. ’Choose atomic formula not containing ’=’ whenever
it is possible’.

9

Further Work

We could study the ’ordering’ further, but there is the danger that we will try
to ﬁnd some deep relations in results of quite a superﬁcial learning. The plan israther to try some less trivial learnings, e.g. to add some other attributes of proof
situations and to include the heuristics found so far (here it would be the ’ordering’ found) to the set of possible solutions, and in longer term to try automating
the process of succesive learnings to create some hierarchies of heuristics.

10

Acknowledgements

I would like to thank doc. RNDr. Petr Štěpánek, DrSc. for advice and help
with this work, and also doc. RNDr. Olga Štěpánková, CSc., from the Czech
Technical University for providing contact to the Esprit Project 20237 Inductive
Logic Programming II. Many thanks to people working on Progol and on the
MIZAR project for making their software publicly available.

18References[1] [Bundy 83] Bundy, A. The Computer Modelling of Mathematical Reasoning.
Academic Press, 1983.
[2] [Chang and Lee 73] Chang C-L. a Lee R. C-T. Symbolic Logic and Mechanical
Theorem Proving. Academic Press, 1973.
[3] [Jirků a kol. 91] Jirků, P., Štěpánek, P., Štěpánková, O. Programování v
jazyku Prolog. SNTL - Nakladatelství technické literatury, 1991.
[4] [Lenat 78] Lenat, D.B. The Ubiquity of Discovery. Artiﬁcial Intelligence 9:257-285, 1978.
[5] [Muggleton 95] Muggleton, S. Inverse Entailment and Progol. New Generation
computing, 13 (1995), p. 245-286.
[6] [Roberts 97] Roberts, S. An Introduction to Progol. Article from Progol home
page, 1997, ftp://ftp.cs.york.ac.uk/pub/ML GROUP/progol4.2/manual.ps[7] [Rudnicky 92] Rudnicky, P. An Overview of the MIZAR Project. Article fromMIZAR home page, 1992, ftp://ftp.cs.ualberta.ca/pub2/Mizar/httpd/htdocs

19Appendix A
The theorems and deﬁnitions used in the proof of Rolle’s theorem.
+AXIOMS 13
AXIOMS 22+BOOLE 29
BOOLE 8
+FCONT 1 30
FCONT 1 def 2+FDIFF 1 16
+FDIFF 1 20

FDIFF 1 30
FDIFF 1 def 8+FUNCT 1 102+NAT 1 18
NAT 1 19
+NAT 1 21+NAT 1 38+PARTFUN2 57
RCOMP 1 11
RCOMP 1 15
+RCOMP 1 24
+RCOMP 1 25
+RCOMP 1 28
RCOMP 1 6
RCOMP 1 7
REAL 1 14
REAL 1 26
REAL 1 33
REAL 1 39
REAL 1 50
REAL 1 53
REAL 1 59
REAL 1 66+REAL 1 67
+REAL 1 72
REAL 1 73
REAL 1 83+REAL 1 92
+RFUNCT 2 10
RFUNCT 2 18
+RFUNCT 2 19

x+(y+z)=(x+y)+z.
x ≤ y & y ≤ z implies x ≤ z;
X c= Y & Y c= Z implies X c= Z;
x ∈ X U Y iff x ∈ X or x ∈ Y;
Y c= dom f & Y is compact & f is continuous on Y implies (f(Y)) is compact;
pred f is continuous on X means X c= dom f & for x0 st x0 ∈ X holds f|X
is continuous in x0;
f is differentiable on Z iff Z c=dom f & for x st x ∈ Z holds f
is differentiable in x;
for f,x0 for N being Neighbourhood of x0 st f is differentiable in x0& N c= dom f holds for h,c st rng c = {x0} & rng (h+c) c= N holdsh" (f.(h+c) - f.c) is convergent & diff(f,x0) = lim (h" (f.(h+c) - f.c));
Z c= dom f & f is constant on Z implies f is differentiable on Z & for x st
x ∈ Z holds (f‘3Z).x =0;
func f‘3X -> PartFunc of REAL,REAL means dom it = X & for x st x ∈ X holds
it.x = diff(f,x);y ∈ foX iff ex x st x ∈ dom f & x ∈ X & y = f.x;
for k holds 0 ≤ k;
0 <> k implies 0 < k;0 <> k + 1;
k < n + 1 iff k ≤ n;
f is constant on X & Y c= X implies f is constant on Y;
for g,s st g≤s holds [.g,s.] = ].g,s.[ U {g,s};(p<g implies ].p,g.[<>∅) & (p≤g implies p∈[.p,g.]& g∈[.p,g.] & [.p,g.]<>∅ & ].p,g.[ c= [.p,g.]);for s,g st s≤g holds [.s,g.] is compact;
for p,q st p<q holds ].p,q.[ is open;(ex r st r∈X) & X is compact implies X is bounded;[.g,s.] = {r : g≤r & r≤s };].g,s.[ = {r : g<r & r<s };x-y=x+ -y;-0=0;
x<>0 implies (1/x=x" & 1/x"=x);y<>0 implies (-x/y=(-x)/y & x/(-y)=-x/y);x≤y iff -y≤-x;x ≤ y iff x+z≤y+z;
x<y implies x+z<y+z & x-z<y-z;x < 0 iff 0 < -x;((x<y & z≤t) or (x≤y & z<t) or (x<y & z<t)) implies x+z<y+t;
0<z implies 0<z";
0<z implies (x<y iff x/z<y/z);-(x-y)=y-x;((x ≤ y & z ≤ t) implies x - t ≤ y - z) & (((x < y &z ≤ t) or (x ≤ y & z < t) or (x < y & z < t)) implies x-t < y-z);
seq.n ∈ rng seq;
seq is convergent & (for n holds seq.n≤0) implies lim seq ≤ 0;(for n holds seq.n∈Y) implies rng seq c= Y;

20

+RFUNCT 2 42
SEQ 1 7
+SEQ 1 def 8+SEQ 2 10
SEQ 2 2
SEQ 2 31
+SEQ 2 6
SEQ 4 24
SEQ 4 46
+SEQ 4 def 3
SEQ 4 def 4
SEQ 4 def 5+SQUARE 1 12
SQUARE 1 14
TARSKI def 2
ZFMISC 1 37

Y c= dom h & hoY is bounded & upper bound (h(Y)) = lower bound (h(Y))
implies h is constant on Y;
seq is not 0 iff for n holds seq.n<>0;
func seq" -> Real Sequence means for n holds it.n=(seq.n)";0<r1 & r1<r & 0<g implies g/r<g/r1;
g/2 +g/2=g & g/4 +g/4=g/2;
seq is convergent & (for n holds 0≤seq.n) implies 0≤(lim seq);
0<g & 0<p implies 0<g/p;(X is bounded & ex r st r∈X ) implies (lower bound X)≤(upper bound X);
0<r & (for n holds seq.n=g/(n+r)) implies seq is convergent & lim seq=0;
attr X is bounded means X is bounded below & X is bounded above;
func upper bound X ->Real means(for r st r∈X holds r≤it)& (for s st 0<s ex r st(r∈X & it-s<r));func lower bound X ->Real means (for r st r∈X holds it≤r)& (for s st 0<s ex r st (r∈X & r<it+s));x ≤ y implies 0 ≤ y - x;
x/1 = x;func { y, z } -> set means x ∈ it iff x = y or x = z;{x} c= X iff x ∈ X;

21

Appendix B
The statistics of usage of theorems and deﬁnitions in the proof of Rolle’s
theorem.
The ﬁrst number says how many times the rule was really used in the original
proof, the second number says how many times it was possible to apply this rule
( using the program for rule application I created), and the third is the numberof situations in which both ocurred simultaneously, i.e. according to the original
proof the rule should be used, and at the same time according to my program
it was applicable at that place. If everything were ideal, the ﬁrst and the third
numbers should be the same.
[[’RCOMP 1’,’:’,[’25’]],[[’FCONT 1’,’:’,[[’def’,’2’]]][[’RCOMP 1’,’:’,[’24’]][[’RCOMP 1’,’:’,[’15’]][[’RCOMP 1’,’:’,[’6’]][[’FCONT 1’,’:’,[’30’]][[’RCOMP 1’,’:’,[’28’]][[’SEQ 4’,’:’,[[’def’,’3’]]][[’SEQ 4’,’:’,[’24’]][[’RFUNCT 2’,’:’,[’42’]][[’PARTFUN2’,’:’,[’57’]][[’REAL 1’,’:’,[’73’]][[’REAL 1’,’:’,[’67’]][[’SEQ 2’,’:’,[’2’]][[’RCOMP 1’,’:’,[’7’]][[’FDIFF 1’,’:’,[’30’]][[’FDIFF 1’,’:’,[[’def’,’8’]]][[’RCOMP 1’,’:’,[’11’]][[’BOOLE’,’:’,[’8’]][[’TARSKI’,’:’,[[’def’,’2’]]][[’SEQ 4’,’:’,[[’def’,’5’]]][[’FDIFF 1’,’:’,[’16’]][[’NAT 1’,’:’,[’19’]][[’SEQ 1’,’:’,[’7’]][[’NAT 1’,’:’,[’21’]][[’SEQ 4’,’:’,[’46’]][[’NAT 1’,’:’,[’18’]][[’REAL 1’,’:’,[’53’]][[’NAT 1’,’:’,[’38’]][[’AXIOMS’,’:’,[’13’]][[’SEQ 2’,’:’,[’10’]][[’SQUARE 1’,’:’,[’14’]][[’REAL 1’,’:’,[’92’]][[’SEQ 2’,’:’,[’6’]][[’AXIOMS’,’:’,[’22’]][[’REAL 1’,’:’,[’59’]][[’REAL 1’,’:’,[’14’]][[’FDIFF 1’,’:’,[’20’]]

1,2,1].
1,12,1].
1,1,1].
2,4,2].
1,10,1].
1,1,1].
1,1,1].
1,3,2].
1,0,0].
1,2,1].
1,2,1].
1,143,2].
2,46,6].
2,1072,20].
1,9,0].
1,362,3].
1,950,13].
1,12,2].
1,48,4].
1,3824,40].
2,0,0].
1,3,1].
8,20,8].
4,0,0].
10,20,10].
4,380,16].
4,8,4].
4,56,20].
4,28,4].
14,28,14].
4,9,8].
4,1068,28].
2,16,12].
12,22,20].
8,52,0].
6,3,0].
4,34,6].
4,21,16].

22

[[’RFUNCT 2’,’:’,[’18’]][[’FUNCT 1’,’:’,[’102’]][[’SEQ 4’,’:’,[[’def’,’4’]]][[’SQUARE 1’,’:’,[’12’]][[’REAL 1’,’:’,[’83’]][[’SEQ 1’,’:’,[[’def’,’8’]]][[’REAL 1’,’:’,[’26’]][[’REAL 1’,’:’,[’50’]][[’REAL 1’,’:’,[’72’]][[’REAL 1’,’:’,[’39’]][[’REAL 1’,’:’,[’33’]][[’REAL 1’,’:’,[’66’]][[’RFUNCT 2’,’:’,[’10’]][[’RFUNCT 2’,’:’,[’19’]][[’BOOLE’,’:’,[’29’]][[’ZFMISC 1’,’:’,[’37’]][[’SEQ 2’,’:’,[’31’]]

2,0,0].
5,13,5].
2,0,0].
4,8,8].
2,32,4].
4,18,12].
14,360,20].
14,52,4].
4,2,2].
2,46,4].
4,1016,20].
2,36,0].
10,8,8].
4,12,4].
7,17,7].
4,22,0].
2,0,0].

23