A Theorem Prover for Elementary Set Theory

1. Introduction

This is a report of some of our research car­ ried out mainly during the summer and fall of 1974, it describes an implementation of a theorem prover based on truth value preserving transformations which has been applied to proving theorems in the domain of elementary set theory.

In section 2 we describe the basic deductive system, and in section 3 we present some protocols produced by tha theorem prover while trying to prove some theorems of set theory. Finally, in section 4 we draw a few conclusions.

2. Description of the Theorem Prover

Our theorem prover consists of an interpreter for mathematical expressions and many items of mathematical knowledge. This interpreter is a fairly complex mechanism, but it may be viewed as applying items of mathematical knowledge of the form ~ ++ ~ or ~ = ~ to the theorem being proven, in the following manner: The interpreter evaluares the theorem recursively in a call-by-need manner. That is, if (fa 1 ··. a) is a sub-expression being evaluated, then the ninterpreter tries to apply its items of knowledge to that sub-expression before evaluating the arguments a 1 ··· a. For each sub­ expression that the interpreternevaluates, in turn it tries to match the ~ expression of an item to that sub-expression. If, however, during the application process an argument a . does not match the corresponding argument of the 1 ~ expression, then a. is evaluated, and the system then tries to match fhe result of that evaluation. If ever the interpreter finds a sub-expression ~a which is an instance of ~ of some item, then it replaces that expression by the corresponding instance ~a of ~. At this point all memory of the sub-expression ~a is immediately lost and the interpreter now evalu­ ates ~a. If no items can be applied to a sub­ expression then the sub-expression is not evalu­ ated again but is simply returned.

For example if {x} = {y} ++ x = y and {x} = {x} ++ · are the only items and if they are listed to be used in that order then evaluating the theorem {A} = {A} V A 1 A will cause the sub­ expression {A} = {A} to be replaced by A = A re­ sulting in A= AVA 1 A. All memory of the sub­ expression {A} = {A} is immediately lost upon its replacement by A = A and thus the interpreter does not attempt to apply the second item to {A} = {A}.

A THEOREM PROVER FOR ELEMENTARY SET THEORY

Department of Artificial Intelligence University of Edinburgh

F. M. Brown Scotland

Sometimes it will be the case that our interp­ reter will need to use items which are only valid in certain sub-domains of a given domain. For example, if we wish to use an item ~x ++ ~x (or ~x = ~x) where x is restricted to the sub-domain rrx, then we represent it by a conditional item:

ITx + (~X ++ ~X) (or ITX + ~X = ~X)

The interpreter handles conditional items in the same way in which it handles non-conditional items until it has found a ~a which matches the sub-expression being evaluated. At this point on a conditional item, the interpreter tries to match each element in the conjunction ITx with some ex­ pression which it believes to be true. If such matches are found with substitution acr then ~acr is returned. Otherwise the interpreter tries to apply another item as previously described.

The use of conditional items provides a gen­ eral method of restricting the free variables of an item to a particular sub-domain. Its only dis­ advantage is that the amount of extra matching it forces the interpreter to perform. In order to minimize the amount of matching on the most common sub-domains we allow those sub-domains to be in­ dicated by a particular style of variables.

For example, the automatic theorem prover de­ scribed in this paper which is based on the set theory system described in Quine's [1969] book Set Theory and its Logic involves two domains: The larger domain, is the domain of abstracts, where an abstract of any propositional function fx with one free variable x is simply: {x: fx}, and the smaller domain is the domain of sets where a set is nothing more than an abstract a which exists; that is where 3x x =a is a theorem of Quine's system.

Roman letters are used to indicate the sub­ domain of sets whereas Greek letters are used to represent both sets and other abstracts.

An informed reader will recall that tables of re-write rules (rather simple items represented in ones mathematical language), and other items were used in many of Bledsoe's theorem provers [1971, 1972], and that Boyer and Moore [1973, 19741 used a symbolic LISP interpreter to order the applica­ tion of various recursive definitions, re-write rules, and induction rules. More recently Aubin [1976] has also used a symbolic interpreter for much the same purpose. Our interpreter for mathe­ matical expressions has also been ·used in other mathematical domains (Brown [1976]).

This theorem prover includes both logical and set-theoretic knowledge. We first describe the items of logical knowledge, and then the items of set theoretic knowledge.

2.1 Logical Knowledge

Our theorem prover has knowledge about twelve logical symbols which are listed below with their English translations:

1\ and

:::> implies

V or

++ iff

"' not there exists

· true V for all

c false equal

+ implies (This symbol is called a sequent arrow)

and and (This symbol is used to form an implicit conjunction of sequents)

The sequent arrow may be defined as follows: <j>l ··· <j>n + ljJl ... ljJh =df(<j>l/\ ... 1\<j>n) ::>(ljJlv' ... VIjJn) where <j>i and ljJj are sentences. Thus a sequent may be thought of as being a database of statements <j>l, ··· , <j>n called assertions which occur before the sequent arrow, and statements ljJl, ··· , ljJn called g.oals which occur after the sequent arrow.

The items of logical knowledge, which are all schemata because they involve ellipses (i.e. dots representing arbitrary expressions), are listed below:

Assertion schemata :

· +: ( ...... + .. )++( .... + .. )

c +: ( .. c .. + .. )++·

"' +: ( .. 'VX .. + .. )++( .... +X .. )

1\ + : ( .. X"Y .. + .. )++( .. X,Y .. + .. )

V +: ( .· XvY. ,+, .)++( ·· x ·· + ·· )and( ·. Y ·. +,,)

:::> +: (' ·· X=>Y ·· +,.)++( ···· +X ·· )and( ·· Y ·· +,.)

3 +: ( .. jx <j>x .. + .. )++( .. <j>f* 1 ... * ) .. + .. ) where f is a new skolem nfunction and · 1 .·· *n are all the unification variables*

which occur in <j>x.

where f is a skolem function not occurring in t. This is our version of the Law of Leibnitz, for example:

(A B V C + C <;. A) ++ (+ C <:::, B U C)

Goal schemata:

+ 1111: (. ,+,. II! ·· )++ ..

where f is a new skolem function and * 1 ·.· *n are ~11 the unification variables*

which occur in <j>x.

Other logical schemata:

where l<i~n and e is any one of the substitutions which satisfy both the forcing restriction and the instantiation restriction. These two restrictions are described below.

*Unification variables are those variables pro­ duced by the V + and + 1 items and which may later be instantiated by the Unify item (i.e. the Unify

Schemata).

The forcing restriction is the requirement that the substitution e makes tautologous the greatest number of sequents starting with the first sequent and progressing towards the nth sequent. That is, the substitution e makes the first i-1 sequents tautologous, and there is no substitution which makes the first i sequents tautologous. The rational behind this restrictb~ is similar to Bledsoe's [1971, 1972] ideas on forc­ ing, in that we force each sequent to make its con­ tribution to e and then throw it away. In the case that there actually is some substitution which will make all the sequents tautologous, without further unification variables being created (by the V + and+ '3 items which will be described later in this section) this restriction leads to a complete proof procedure, in that e will be one such substi­ tution. As a minor point, if 9 makes all the sequents tautologous, then this item is defined to return ·· An example instance of this item illustrating the forcing restriction is: [(P* + Pa,Pb)and(Q* + Qb) and R* + Ra)]++(Rb + Ra) We call any strategy which chooses the ordering of the sequents to which the unify item is applied, a forcing strategy, and will later discuss our forc­ ing strategy.

The instantiation restriction is the require­ ment that no unification variable be instantiated to a term whfch already occurs in the list associ­ ated with the quantifier from which that unifica­ tion variable was produced by an application of either the V + item or the + j item. The rational behind this restriction is that if a term t is al­ ready in the list associated with a quantifier such as V in ( .· Vx<j>x · . + ·· ) then <j>t has already been produced in that sequent, and hence producing an­ other <j>t by instantiating * to t could only be

redundant.

The list of terms associated with a quanti­ fied formulae such as (Vx<j>x) essentially represent the instances .pt 1 ··· <j>t of it that have been pro­ duced. This list is st2red by appending it onto the end of a list containing the bound variable x as in: (V(x t 1 .·· t) <j>x). An example of the use of this restrict~on is the following instance of the Unify schemata:

where * is a new unification variable and no more than one Unification variable occurs in (x ··· ) ·

where * is a new unification variable and no more than one Unification variable occurs in (x ... ).

In the last two items we have seen formulae of the form V(x ·.. )<j>x and 3(X ··· )<j>x which are not usually thought of as being well formed sentences of logic. Such formulas should be interpreted as respectively Vx<j>x and ]x<j>x which are well formed sentences of logic. The ··. list is used merely to store certain pragmatic information used by the deductive system. This information is simply the list of instantiations of the Unification variables that were produced from this quantifier by applications of the V + or + 3 item. This pragmatic in­ formation is kept in order to be able to check the instantiation restriction, when using the Unify item (i.e. the Unify schemata), and in order to check the restriction on the V + and + 3 items that no more than one unification variable may already occur in the (x ... ) list. This last requirement is called the variable restriction. The rational behind this restriction is that there is no way in which three instances ~* 1 , ~* 2 , ~* 3 of a formulae ~x could interact so as eo bind at least one of those unification variables, that could not be obtained by initially using only two instances and and then creating a third instance only after one of the first two unification variables is bound. An example of the use of this restriction is the fact that the + 3 item could not be applied to the sequent: (+ (3 (x* 1 * 2 )~ )

The logical items are not all used at the same time. In particular the V +, + ~ and unify items are used in a special way. Initially, the interp­ reter evaluates each sequent trying to apply the items in the following order:

1. Non splitting assertion items:

~, t:J.+., 1'\.r+-, A-+, ]-+, =+

1. Non splitting goal items:
2. -+· I -+Jl I -Y'I,, -+ " I -+ ;) , -+V
3. (N(3) Non logical items
4. The atom and "and" items
5. Splitting assertion items: V+, :;, +, ++ +
6. Splitting goal items:
7. +I\, + ++
8. (B) The Unify item
9. (C) The V + and +3 items once.
10. (A) The group (A) of items are applied first and are used in what is the normal evaluation process in a call-by-need manner. The sub-ordering from (1) to (6) reflect the fact that we try to delay splitting as long as possible, and within that restriction, try to work on assertions in a sequent, before working on goals. A reason for preferring to work on assertions first is that applications of the = + item can often simplify the problem a great deal. A simple reason for delaying split­ ting and applying the other items first is so that we don't have to apply those items twice after the split to each sequent separately. However, we find that the time gained by not having to apply items a second time,seems to be balanced by the time lost necessary to effect the delaying operation. A more substantial reason for delaying the split­ ting items is to handle certain subtle interactions between the +V, 3+, +3, and V+ items necessitated by the incompleteness caused by the forcing restric­ tion. These interactions will be described later in section 3 when we discuss our proof of Cantor's
11. theorem.
12. (B) After the items of group (A) have been applied as many times as possible, the interpreter then tries to apply the unify item to the particular re­ ordering of the conjunction of sequents, that is determined by the forcing strategy. The forcing strategy we have used is this: The conjunction of sequents are re-ordered such that those sequents which contain formulas beginning with a quantifier such that the quantifier
13. satisfies the variable restriction and
14. (2 ) has the shortest associated list· of in­ stantiations of any sequent in the con­ junction.

are at the end, and hence will be unified last. The rational behind our forcing strategy is that eachquantifier should get its fair chance to con­ tribute instances towards proving the theorem. Thus, for example, if we forced out a sequent (by unifying it first) containing a quantifier which had not contributed any instances yet, and if that quantifier was actually needed in order to ·prove the theorems, then it is very probable that the substitutions made in unifying that sequent are irrelevant and in fact detrimental to solving the other sequents in the conjunction of sequents. An example of the effect of our forcing strategy is

to re-order:[(Qa+3 (x * 1 )Q* 1 land(Qb+3(x * 1 s)Q* 1 lJ

• (C) Next, if the application of the unification item does not result in ·, then the interpreter picks a sequent from the conjunction of sequents and tries to apply the V + and 3 + items once to each formula in the sequent which begins with a quantifier such that, the quantifier has the fewest number of terms in its associated list of any quantifier which satisfies the variable restriction in that sequent. We call this strategy for creat­ ing unification variables the creation strategy. The process of applying items then repeats itself starting at step (A) . Note that a quantifier followed by only a variable, not a list, counts as having zero terms. Thus, for example, the creadon strategy implies that only the V + item would be applied to the sequent:

( (Yx Px) + (3 (xa) Qx), (3 (y*) Qy))

The rational behind the creation strategy is that for each sequent it simply implements a breath first method of creating unification variables from the quantifiers in that sequent. This strategy is initially, therefore, the method that one unification variable will be created for each quantifier, before a second unification variable is ever created in that sequent. It differs from such a method in that if the theorem cannot be proven with a single unification variable for each quantifier, then it does not fail but continues to create more instances as called for by the creation strategy. This allows us, for example, to prove theorems which need multiple variables from their quantifiers such as Example 2 given in section 3.

Finally, if the application of the unification item of step (B) resulted in · then the processes terminates because the theorem has been proven.

An informed reader will recall that these prop­ osi tiona! rules are used in Wang · s algor.i thm in the LISP 1.5 manual [1965], and that Wang [1960] used the other rules . restricted tothe decidable case of where only skolem constants, but not skolem func­ tions were necessary. The general idea of unif­ ication is due to Prawitz [1960]who used rules sim­ ilar to all the rules given here except for = + and unify. His unification rule leads to a complete logic, ours does not. Robinson [1965] clarified Prawitz's unification algorithm by re-defining it, as we have done, in terms of skolem functions, rather than in terms of ordering restrictions on Prawitz variables and skolem constants. More recently Bibel and Schreiber [1974] have implement­ ed a complete sequent logic.

2.2 Set theoretic knowledge

Our theorem prover has knowledge about one primitive set theoretic symbol: E which is in­ terpreted as: is an element of, and knowledge about a large number of defined symbols. Some of these defined symbols along with their definitions and English translations are listed in table 1. In that table, the name of each expression usually indicates where that expression may be found in Quine's [1969] book: Set Theory and its Logic. For example, the definition of the symbol ~ whose name is Q2P5 is expression number 5 in chapter 2 of that book. Note that a definition essentially defines the expression on the left side of the outer most ++ or = sign in terms of the expression on the right side.

With the sole exception of the axiom of exten­ tionality, there are four kinds of items of set theoretic knowledge used by our theorem prover. They are: definitions, reduction lemmas, existence axioms, and existence lemmas. As previously mentioned some of the definitions that were used are listed in table 1. Some reduction lemmas that were used are listed in table 2. Some existence axioms that were used are given in table 3, and some existence lemmas that were used are given in table 4.

Definitions and Reduction lemmas are of the forms~++ w,~ = w, IT+(~++ W),or IT+ (~= Wl· Existence axioms and existence lemmas are of the form: ~EV where V is the universal abstract.

The definitions and reduction lemmas are used only as items by the interpreter to evaluate sub­ expressions, as described at the beginning of section 2.

For any given sub-expression that is being evaluated the interpreter tries to apply the defin­ itions and reduction lemmas in the following order:

first: Q2Pl

then: All reduction lemmas in reverse order from that listed in Table 2.

and finally: all other definitions. For example, since the definition Q9Pl is tried only after the reduction lemma Q9P3, <xy> = <uv> evaluates to x = uAy = v using Q9P3 and not to ({x}={u} /\ {x y};.{uv}) V({x}={uv}A {xy}={u}) using Q7P9 via definition Q9Pl.

The philosophy behind restricting definitions and reduction lemmas to being used only as items is two.fold : First, since the transformations made by the interpreter are truth value preserving as­ suming our axioms of set theory (and in the case of conditional items also assuming the particular sequent in which the sub-expression being evaluat­ ed occurs) the resulting sequent is a theorem of our set theory iff the original sequent was a theorem of our set theory. Second, at least in the case of definitions (because after all they are definitions and hence can be eliminated), we know that· in a certain sense the complexity of the resulting expression is less. This fact, combined with the manner in which the sequent calculus it­ self reduces the complexity of its sequents, means that the resulting expressions are becoming less complex.

Furthermore, in the case of reduction lemmas such as ~ ++ w, if the ~ expression contains at least one symbol which was defined later than any symbol in w, then it is quite probable, but not at all certain, that the above termination property will hold. For example, all the non-conditional reduction lemmas in table 2 contain a later de­ fined symbol in their ~ expression, and thus the use of such items probably will reduce complexity. Thus our philosophy for using reduction lemmas as items is basically the same as for our use of de­ finitions as items.

It should be noted that several people have considered the problem of proving that various sets of reduction lemmas preserve termination when used in this manner, notably Plotkin [1972], Lankford [1975] and Siekmann [1973].

It should not be thought that the termination property must hold in all cases for it to be useful to use reduction lemmas in this manner, for it may be the case that it fails only for pathelogical expressions which are of little interest in mathe­ matics. An example of this is the fact that Q2Pl fails to reduce complexity when y is replaced by the following name in ZF of the null set: {x:xEx}.

The existence axioms and the existence lemmas are used to increase the range of applicability of the logical schema = + the contextual definition Q2Pl and of the reduction lemmas. Namely, when­ ever an expression of the form R E V where R is some abstract is either assumed or proven, then for every combination of variables and abstracts X such that X E V is now known, new versions of Q2Pl and the reduction lemmas are asserted.

Table 2: Reduction Lemmas:

Q7P7: VxYy {x} = {y} ++ x=y

Q7P8A: Vx Vy Vz {xy} = {z} ++ x=z A y=z

Q7P8B: Yx Vy Yz {z} = {xy} ++ z=x I\ z=y

Q7P9: Yx Yy Yu Vv{xy}~{uv}++(x=uAy=v)v(x=vAy=u)

Q9P3: Vx Yy <xy> = <uv> ++ x=u A y=v

Q9PS: Vx Yy <xy> £ {<uv>:$uv} ++ $xy

CRLl: Func .f + (<wy>gf ++ w=f'y)

Table 3: Existence axioms and axiom of

extentionality

Q7PlOA: ¢£V

Q7PlOB: Vx Vy {xy}£V

Q4Pl: Vx Vy Vz (x=y ". X£Z. :J ygz)

Table 4: Existence Lemmas:

Q7Pl2:

Q7Pl3:

E2:

{a}£V

{af3}£V

<af3>£V

A simpler method of implementing the addition of these new reduction rules, is to agree that the initial universally quantified variables of a de­ finition or a reduction lemma are allowed to match, not just variables, but also any abstract R such that R £ V is known.

There is one further way in which the exist­ ence axioms are used, and this has to do with the fact that they are axioms. For this reason, if the interpreter gets "stuck" while trying to solve a sequent (that is, if no items can be applied to that sequent) in proving a theorem, it will in privitive notation, i.e. with the defined symbols eliminated, add each axiom as an additional hypothesis in that sequent.

Again an informed reader will recall Bledsoe's set theory theorem prover [1971].

3. Example

We give below a protocol produced by our theorem prover while proving Quine's version of Cantor's Theorem. We have listed on the right the name of the item which was applied to each sequent in the protocol · Any name which is starred: '*' is the name of a lemma. A list of names indicates the use of a reduction lemma cor­ responding to the item named by the first name in the list, and created by the items named by the remaining names in the list.

The protocol is presented as a tree of sequents, grown top down, starting with the sequent contain­ ing only the theorem the system is trying to prove. On each line of the proof the item name following the colon indicates that that item was applied to the sequent on that line, producing the sequent on the line immediately below that one. In the case of a logical split item (+I\, + ++, V +, :::> +, ++ +) two sequents will be produced, and they are indicated by drawn arrows.

The proof is segmented by the scope of attempted applications of the Unify items. The boundaries of each segment are indicated by stat­ ing where each segment starts. That is by stating:

:0k starts here

where k refers to segment k. The system attempts to apply the Unify item once to a sequence of all endsequents of each segment. Thus, every sequent

1. · ® . Q) · @ ,Func f.* s£ (a* 2) · *SEan { y:'Vy£* 2 'y}. * 4 £a* 2 ++* 4 £f 1 (b* 2 l, (b* 2 )£a + :Q2PS
2. <I),@ ,d),@ ,Func :F,\£(a* 2 ), *sdx:x£al\ xdy:<vy£* 2 1 Y}, * 4 £ (a* 2 l++* 4 £t 1 (b* 2 l, (b* 2 )£a +
3. Q),C6),Q),@,Func f,*s£(a* 2 ), \Ea;l\ *s£{Y="'Y£*2 1 y}t4£(a*2)++*4£il (b*2), (b* 2 )£a +
4. GJ, <1), Q), ® ,Func f,*s£ (a* 2 l ,*sEa, *sdY="'Y£*2 ly},* 4£ (a*2l++* 4£fl (b*2l' (b* )Ea +

:Q2P1

:Q2P1

• Q),@ ~ (;D,@ ,Func f,\£ (a* 2 l ,*sEa, "'*s£*2 1 *s,*4£(a*2)++*4£fl (b*2), (b*2)£a _,. '"' +
• Q),@, <1),@ ,Func f,*s£ (a* 2 l ·*sEa., * E(a* )++* £f 1 (b*) (b* )Ea + * £* 1* 4 2 4 2 I 2 . /~ 2 S :++ +
• / -- -------- (!),@,a>,@ ,Func f.,*s£ (a*2 l ,*sEa, ~ * 4 £(a* 2 l ,* 4 £f 1 (b* 2 l, (b* 2 l£a + *s£* 2 1 *s :Unify [*2=f,*4=*s·*s=<b*2>J ·
• _,. *s£*2 1 *s,*4£(a*2l'*4£fl (b*2l [*4=*sJ · :Unify
• (i) , (2), Q),@) ,Func f,* 4 £(a* 2 l++* 4 £f 1 (b* 2 l, (b* 2 > Ea + *s£ (a* 2 ) ,*sEa n{y:-vy£* 2 1 y} :Q2PS
• OJ ,@, Q),@ , Func -f-,* 4 £ (a* 2 l++* 4 £f 1 (b* 2 l, (b* 2 l£a+ *s£(a* 2 l ,*s£{x:x£aAx£{y:<vy£* 2 1 y}}:Q2P1
• !P 1 ~ 1 ())I@ ,FunC f,* 4 £(a* 2 )++* 4 £f 1 (b* 2 > I (b*2)£a+*s£ (a*2l ·*s£aA*s£ty:<vy£*2 ly} :+/\
• Q:· ,@ , @),@ ,Func ~.* 4 £ (a* 2 )++* 4 £f 1 (b* 2 l, (b* 2 )£a + *s£(a* 2 ), *sEa =~-+
• (jJ ,(2),0),@ ,Func f,* 4 £(a* 2 ),* 4 £f 1 (b* 2 ), (b* 2 )£a + *s£(a* 2 ), *sEa [* =* Jor [* =(b* )J 4 s · s 2
• *s£a,*4£(a*2), *4£fo1 (b*2) [*s=<b*2>J :Unify I .---------- I

:Q2P1

:+"'

1. , @ , ® .'@ ,Func f, * 4 £ (a* 2 l++* 4 £f 1 (b* 2 l, (b* 2) £a+* s£ (a* 2), * sdy:'Vy£* 2 ly}
2. ~, ~,@,@ ,Func f,* 4 £(3.* 2 l++* 4 £f 1 (b* 2 l, (b*2) £a+*S£ (a* 2) ,'V* S£* 2 1 * S

~

*s£*2 1 *s+*s£(a*2l ,*4£(a*2l ,*4£fl (b*2l

G:· 1 (2! 1 Q:l 1@ ,FunC f, (b* 2 )£a 1 *s £* 2

[*2=f,*4=*s·*s=(b*2>J

·

• ~· , @·· , @ ,Func f .... * £ Pa 1
• ~ . ~ . cr· ,Func f .... * 1 dx:x.;:: a}
• (j) , @ , (3) ,Func f .... *1 c;:; a
• (i) , c~ , cr; ,Func f + Vx X£* 1 :=> x£a

:Unify

:01

:Q2P1

:Q2P2

:+ "

1. I (~ (."' I._} ,Func f .... (c*1)£\::. (c\)Ea :82 starts here :+'J

li\ 6 ·

f -3·, F

f

( * ) * + ( * )

1. , R; , Q. ,*3£(a*2)++*3£a"{y:<vy£*21y}, Func f, (c*1 )£*1 + ~c-~-
2. ""' , ,~ , , _. , unc , c 1 £ 1 c 1 £a :++-+
3. Q;; , @ , <I· , * 3 £ (a* 2 ) , * 3 £a fl { Y: "'Y£ * 2 1 Y} , Func f,(c* 1 ) £* 1 + (c* 1 )£a

:V+

:Q2PS

1y}} 1

:Q2P1

• Func f, (c* 1 )£* 1 + (c* 1 )£a (j) 1 ~ 1 (j) 1 * 3 £ (a* 2 ) 1 * 3 £a 1\ * 3 £{ Y : 'Vy£ * 2 1 Y} 1 :/\ +

\P , @ , Ql ,* 3 ~(a* 2 l ,* 3 dx:x£aAxdy:<vy£* 2

• Func f,(c* 1 )£* 1 + (c* 1 )£a
• Q:j 1 ~) 1 Q) I* 3 £ (a* 2 > '* 3 £a I* 3 £{y :'Vy£* 2 1 Y} I Func f, (c* 1 )£* 1 + (c* 1 )£a
• Q;, ' ® ' (X. ,*3£ (a*2) ,*3£a,"'*3£*2 1 *3, Func .;, (c\) £\ + (c\)Ea
• cr) 1 (~) 1 <1' ,* 3 £(a* 2 ) ,* 3 £a,FUnC f, (c*1)£*1 + *3£*2 1 *3,(c*1)£a [* = (c* ) J 3 · 1

:Unify

.-------------·

:Q2PS

• QJ,Q) ,(}),Func-f,(c\)E\ + (c\)£a, * 3 £ (a* 2 >, * 3 ea ll{y:<vy£* 2 1y}
• @ ,@, Q) ,Func f, (c* 1 )£* 1 + (c\)Ea, * 3 £ (a* 2 >, * 3 dx:x£a/\ xdy:<vy£* 2 1y}}
• d),~, Ql ,Func f, (c* 1 )£\ + (c\)Ea, *3£(a*2) ,*3£a/\*3dy:<vy£*2 1 y}

:Q2P1

:+1\

:Q2P1

· Time = 1,494 milliseconds or approximately: 1~ seconds on a DEClO computer with a KAlO CPU

Note that two distinct instantiations of formulae Q) have been used:

A theorem prover which:

(1) immediately skolemized it's formulae and

(2) allowed no more than one instance of each variable

would not be able to prove this theorem except by a very lucky accident.

The basic problem of this proof is at the start of 81: and is to decide which of the following two formulas to work on first:

(1) ex() {y:'Vye: · 2 'y} e:V

If one begins by splitting on (2) then on each branch of the search space formulae (1) will reduce to

which produces on each branch a distinct* skolem function (a* 2 ), (a'* 2 J, and this will not lead to a proof. Thus one must begin working on the first formulae. However, this first formulae in a few steps reduced to @ . If x in Q) is immediately replaced by a single Unification variable, then again no proof will be obtained, for we have seen that from our proof that two variables * and * bound to distinct skolem functions c and 3 b were 5 needed.

Thus what one must do is to start on formulae

*It is not obvious that two quantifiers on differ­ ent branches of the search space could be replaced by the same gensymed skolem function, in a system with unification variables because instantiating them can cause these skolem functions to appear in the same sequent.

(1), then switch to formulae (2) and split, and then come back on each branch and instantiate (1).

4. Conclusion

We have described an automatic theorem prover for the domain of elementary set theory, and have presented some protocols of its behaviour when proving some theorems. we wish to stress that the program is fast and compact. For example,we have seen that it took less than 2 seconds to obtain a proof of Cantor's Theorem. It should be noted that our theorem prover is implemented in compiled UCI LISP (Bobrow [1973]) and was executed on a DEClO with a KAlO CPU.

Acknowledgements

I thank Bernard Meltzer, Robert Kowalski and Raymond Aubin for many enlightening discussions · This research was supported by a scholarship awarded to the author by the University of Edin­ burgh, and is currently, supported by a grant BRG 94431 from the Science Research Council.