The Markgraf Karl Refutation Procedure

THE MARKGRAF KARL REFUTATION PROCEDURE (fALL 1981)

K. Blasius, N. Eisinger, J. Siekmann, G. Smolka, A. Herold, C. Walther

Institut fur Informatik I UNIVERSITAT KARLSRUHE D- 7500 Karlsruhe, Postfach 6380

Abstract : The cuPrent state of a TheoPem Proving Sys tem (The MaPkgmf KaPt Refutation FPocedure) at the UnivePsity of KaPtsPUhe is pPesented. The goat of this pPoject can be swrurrJ.rized by the fotl-owing thPee cl-aims: i t is possibLe to progpam a theoPem proveP (TPJ and augment it by appPopPiate heuristics and domain-specific knowLedge such that

• (iJ it witt displ-ay an 'active' and directed be­ havioUP in its striving foP a pPoof, PatheP than the 'passive' combinatorial- seaPChthPough very taPge seaPch spaces, which was the cha­ Pacteristic behaviouP of the TPs of the past. Consequentl-y
• (ii) it witt not genePate a seaPCh space of many thousands of iPPetevant cl-auses, but witt find a proof with comparativel-y few Pedundant de­ Pivation steps.
• (iii) Such a TP witt establ-ish an unprecedented l-eap in pePformance oveP previous TPs e;rppessed in terms of the difficuLty of the theoPems it can prove.

The resuLts obtained thus far coPPOboPate the first two claims.

0. INTRODUCTION

The working hypo thesis of this TP project [DS77], [ DS79], first formulated in an early proposal in 1975 , reflects the then dominating themes of artifi­ cial intelligence research, namely that TPs have a ttained a certain level of performance, which will not be significantly improved by:

• (i) developing more and more intricate, refinement strategies (like unit preference, linear reso­ lution, TOSS, MTOSS, ... ),whose sole purpose i s to reduce the search space, nor by
• (i i ) using different logics (like natural deduction logics, sequence logics, matrix reduction methods etc)

a lthough this was the main focus of theorem proving r e sea rch in the past.

The relative weakness of current TP-systems as com­ pared to human performance is due to a large extent t o their lack of the rich mathematical and extrama­ tematical knowledge that human mathematicians have : in particular, knowledge about the subject andknow­ l edge of hpw to find proofs in that subject.

Hence the object of this project is to make this knowledge explicit for the case of automata theory, to find appropriate representations for this know­ ledge and to find ways of using it. As a testcase and for the final evaluation of the projects success or failure, the theorems of a standard mathematical textbook [DE71] shall be proved mechanically.

In the first section of this paper we give a generru overview of the system as it is designed, albeitnot completed. The second section concentrates on those parts of the system, whose implementation is fi­ nished and evaluated. In the third section experi­ mental results are given and the final two sections present an evaluation based on the presentfindings.

I . OVERVIEW OF THE SYSTEM

A BiPd's-eye View

Proving a theorem has two distinct aspects: the creative aspect of how to find a proof, usually re­ garded as a problem of psychol-ogy, and secondly the logical aspect as to what constitutes a proof and how to write it down on a sheet of paper, usually referred to as pPoof theory.

These two aspects are in practice not as totally separated as this statement suggest (see e.g. [SZ69]), however we found it sufficiently important to let it dominate the overall design of the system:

The Supervisor consists of several independent mo­ dules and has the complex task of generating an overall proposal (or several such) as to how the given theorem may best be proved, invoking the ne­ cessary knowledge that may be helpful in the course of the search for a proof and finally transforming both propos~l and knowledge into technical infor­ mation sufficient to guide the Logic Engine through the search space.

The Logic Engine is at heart a traditional theorem prover based on Kowalski's connection graph proof procedure [K075], augmented by several components that account for its strength.

The Data Bank consists of the factual knowledge of the particular mathematical field under investi­ gation, i.e. the definitions, axioms, previously proved theorems and lemmata, augmented as far as possible by local knowledge about their potential use.

A View from a Lesser Altitude

The diagram of figure 2 sufficiently refines figure 1 to gain a feeling for the overall working of the system:

The user types in his problem, gives any possible additional information and advice and then specifies some of the many options open for the final protoali of this session. On the basis of this information the Proposal Generator (PG), which is part of the supervisor, may decide that the theorem is best proved by a general technique like induction, in which case the supervisor loads the induction mo­ dules [CW79] and hands over control. Another in­ stance for the activities of the PG is the follo­ wing: in the case of the presence of equality li­ terals, it discovers this fact and causes the set of clauses to be transformed into a more appropri­ ate set and hands over control to the Equality Reasoning Module. The transformation involves the deletion of certain equality literals (clauses), which are selected for the rewrite-rule-module [HU77], [LA77], [DS79]; other axioms are deleted since they are taken care of by the unification mo­ dule [DS77], whereas certain other axioms are added (e.g . the functional reflexive axioms) to ensure that the resulting set is E-unsatisfiable iff the previous set was unsatisfiable.

If none of the general techniques apply, the Propo­ sal Generator generates a proposal (or several such), which contains heuristic information, of how the theorem may best be proved (e.g. it contains thede­ finitions and lemmata which may be relevant, it suggests some proof techniques which are likely to be appropriate, it suggests which assertion or sub­ problem is best proved first, it tries to generate a t op level plan for the proof if possible and fi­ nally it decides which of the permanent heuristics are to be activated) .

The Proposal Generator has access to two data banks: DATA BANK ONE (DBO) contains the factual mathemati­ cal knowledge like definitions, previously proved theorems and lemmata etc of the particular (ield under investigation (Automata Theory, Abstract Al­ gebra and Set Theory will be considered in the fu­ ture). The PG has to decide which part of DBO is to be activated.

DATA BANK TWO (DBT) contains the mathematical know­ ledge at a conceptual level and the reasoning pro­ cess of the PG is based on these conceptualizations [SIS!).

The proposals are given one at a time to the Technical Assistant (TA), whose task is to transform this information, which up to this point is in­ telligible for a human user, into technical advice and code, which will then govern the top level be­ haviour of the Logic Engine and is for that reason passed on to the Monitor.

The Monitor governs and controls the global beha­ viour of the Logic Engine: immediately after acti­ vation it checks for an easy proof using the ter­ minator heuristic (see section 2) and only upon failure activates the full machinery of the Logi c Engine. Typical control tasks are detecting constant replications of the same lemma, detecting a circu­ lar development in the search space and ke~pingtrack of the 'self resolving' clauses. A good example how the monitor governs the top level behaviour is in its prevention of the unsteady behaviour which the system showed during earlier experimentation: The selection heuristics constantly suggest 'interesting' steps to take and forced the system to vacillate between different parts of the search speace -very unlike the behaviour of people, who, if put into the same situation, would tackle an interesting path until they either succeed or become somehow convinced that it was a blind alley.

Up to this point the decisions and activities of the PG and the TA are to a large extent based on the semantics of the theory under investigation and knowledge about proofs in this theory and their top­ goal may be formulated as: to be helpful "in fin­ ding a proof". Once they have done so, that top­ goal becomes "to derive a contradiction (the empty clause)" and although this goal is of course iden­ tical to the previous one, it impli"es that diffe­ rent kinds of information may be useful: the ori­ ginal information provided by the PG based on the semantics (which is by now coded into various para­ meters, priority values and activation modules) as well as information based on the syntax (of the connection graph or the potential resolvent) .

It may be objected that this is the main goal of a traditional TP also. While this of course true, there is the important difference that a traditio­ nal (resolution based) TP is not dirextly guided towards this goal in a step by step fashion, as no refinement [L078] specifies which literal to re­ solve upon next. For example linear resolution re­ duces the search space as compared to binary reso­ lution, but within the remaining space the search is as blind as ever.

The PG and the TA are currently under development and not implemented at the time of writing.

2. THE LOGIC ENGINE

The Logic Engine is based on Kowalski's connection graph proof procedure [K075], which has several ad­ vantages over previous resolution based proof pro­ cedures: there is no unseccessfull search for po­ tentially unifiable literals, every resolutionstep is done once at most and the deletion of links and subsequently of clauses leads to a remarkable im­ provement in performance, which is heavily exploi­ ted in the Deletion-Module. Most crucial to our approach however is the ohservation that since eve­ ry link represents a potential resolvent, the se­ lection of a proper sequence of links leads to the alleged active, goaldirected behaviour of the sy­ stem.

2. 1 Input and Output

The interactive facilities are too numereous to ac­ count for here and instead a protocol of a typical session is presented at the conference. An intere­ sting point to note is that the interaction at this level was only designed for the intermediate stages of development. It is now to an increasing degree taken over by the Supervisor as it develops, with the intention to move the interface with the user althogether to the outside and to make the Super­ visor take most of the low level decisions. Two sets of instructions however are to stay: the IN-Module is used to set up (and to read) the Data Bank in a way easily intelligible for the user. It also per­ forms a syntactical and semantical analysis of the Data Bank, which is of considerable practical impor­ tance in view of the fact that it eventually con­ tains a whole standard mathematical textbook.

The PROTOCOL-Module provides several facilities for tracing the behaviour of the system at different degrees of abstraction in order to cope with its complexity.

2.2 The Monitor

'I'he deduction steps within the connection graph are governed and controlled by several modules, which are conceptually collected in the MONITOR.

We shall give a brief summary of the task of each of these modules (although each module represents a software development of about the size of a tradi­ tional theorem proving system). Only the heuristic selection functions are presented in more detail be­ low.

The Splitting and Reduction Module is activated first and converts the initial formulas into en­ form subject to possible splitting and reduction operations [BL71]. The resulting set(s) of en-for­ mulas are then transformed into the initial connec­ tion graph(s), which again are substantically re­ duced by subsumption and purity checks [EI81], [WA81] .

The Unification Module contains special purpose uni­ fication algorithms for frequently occurring axioms like associativity, commutativity, idempotence and their combinations, and hence these axioms are re­ moved from the data base prior to activation.

The Refinement Module simulates standard derivation strategies and most of the time only a small frac­ tion of all links in the graph is declared active. For example if only the links emanating from a clause in the initial set of support are declared active and subsequently only the links of each re­ solvent in turn are declared active and the pre­ vious one passive (by appropriate 'on-off-switches'), the resulting derivation is linear. The Refinement­ Module allows to chose among some of the standard strategies and setting refinements [L078]. This has turned out to be advantageous, since it substanti­ ally reduces the number of active links and hence the expense for the computation of the heuristic selection functions and the most successful runs were obtained with this 'mixed approach'. The de­ cision, which refinement to choose, is taken by the Monitor based on some genereal heuristics.

The Planning Module is currently under development and contains additional, heuristically motivated, splitting and simplification routines for the con­ nection graph as well as planning capabilities for proof plans.

The Tracking Module controls the logic engine and detects circular developments in the search space, constant reapplication of the same lemma etc.

The Focussing of Attention Module prevents the un­ steady behaviour mentioned in section one and en­ sures that theorems and lemmas selected by the su­ pervisor are used in preference to other clauses. Both activities are achieved by special weights attached to the links in question.

The Definition Expansion Module exists in a rudimen­ tary form only: as more complicated examples are tried, more refined heuristics are necessary to control the expansion process, i.e. the replacement of the defined literal by its defining clauses.

The Rule Base contains lemmas in the form of a pro­ duction system and each time the if-part is satis­ fied the then-part is added to the current connec­ tion graph.

The Rewrite Rule Module contains simplification and reduction rules in the form of rewrites, which are applied to the terms of the initial graph, as well as to every generated resolvent .

The Deletion-Module heavily exploits the crucial property of this proof procedure that distinguishes it from other proof procedures based on graphs [SH76], [SI76]: the fact that the deletion of links and clauses can lead to a snowball effect of further deletions. Because of this effect it is worth every effort to find and compute as many criteria for po­ tential deletions as possible. At present a clause is marked for deletion if:

• (i) it is pure [WA81]
• (ii) it is a tautology [WA81]
• (iii) it is subsumed by some other clause [EI81]

and this information has absolute priority over the relative priorities to be discussed below.

The Factoring Module controls the factoring of clauses, which is based on special types of links in the connection graph.

In contrast to the global search strategies and global heuristics, the heuristic selection functions of the Heuristic-Module ar.e based on local syntactical information about the graph or the resolvent (Paramodulant) res­ pectiv@!ly · (SS81]. These heuristics--were obtained with two types of experi~~nts: In the first experi­ ment a human testperson is asked to prove a given set of formulas by resolution without any information on the intended meaning of the predicate or function symbols. Then the same set is proved by the system and in case its performance is inferior, the analy­ sis of the deviation (and introspection of the test­ person on why a particular step was taken) can give valueable hints for further heuristics.

In the second type of experiment the system is set to prove a theorem. In the case of success, an ana­ lysis of the protocol, where in the listing of all steps the steps necessary for the proof are marked, provides a remarkably good source of ideas for im­ provement,particularly if the reason why a certain step was chosen, is also printed in the protocol li­ sting.During the last two years several hundreds of such listings were analyzed.

Initially we experimented withabout 20 different heu­ ristic features, where each feature attaches a cer­ tain value to every link kin Gi. Gi is the present graph, Gi+l is the resulting graph after resolution upon linK R and Res is the resolvent resulting from this step:

(£) Sum of literals in Gi+l

(ii) Sum of oZauses in Gi+l

(iii) Sum of links in Gi+l

(iv) Averoge length of oZauses in Gi+l

(v) Average sum of Zinke on ZiteraZs in Gi+l

(iv) Sum (reap. average sum) of oonstant symbols in Gi+l

(vii) Number of distinct predicate ~ymbols in Gi+l

(viii) Number of distinct variables ~n Gi+l

(i:z:) Sum of UteroZs of Res

(:z:) Sum of Zinke of Res

(xi) Sum of constant symbols in Res

(xii) Sum of distinct lklriables in Res

(xiii) Number of distinct predicate symbols in Res

( xiv) Term corrp Ze:z:ity of Res

(:z:v) Minimum of Unks on literals in Res

(:z:vi) CorrpZe:z:ity of the m::Jst general unifier ak attaohed to link k

(:::vii) Age of Res

(:::viii) Degree of isolation of Res

(xi:z:) DegrtZe of isoZation of the parents of Res.

The problem is that although each heuristic feature has a certain worth, the cost of its computation can by far outweigh its potential contribution. Also it may not be independent of the other heuristic fea­ tures; for example features (xi) and (xii) both mea­ sure the "degree of groundness of Res", but in a different way. Similarly the values for Res and for Gi+l are not independent for certain features (e.g. xiii and vii). Also there are the two problems of finding an appropriate metria for each feature and to decide upon their reZative worth in case of con­ flict with other features.

The i nformation contained in the heuristic features is entered in different ways: certain facts (e.g. decreasing size of the graph) have absolute priority and override all other information (see also the merge feature of TT in (DA78]). Most of the informa­ tion of the other features is expressed as a real number in (O,l], where we experimented with several (linear, nonlinear) metrics. This information is then entered in a weighted polynomial and the re­ sulting real number (the priority value) expresse~ the relative worth of the particular link and is attached to each link. In case of no overriding in­ formation the Control-Module selects the link with the highest priority value. Still other information is entered using the "window-technique": among the links whose priority value is within a certain in­ terval (the 'window'), the Control-Module chosesthe one which minimizes some other feature.

The system has been designed such that heuristic features can easily be added and deleted, however after two years of experimentation the system has stabilized with the following solution (stabilized in the sense that neither the addition of heuristks from the above list nor the use of different metrjcs will significantly change the performance of the sy­ stem on an appropriately large set of tests) :

1. Complexity of the Graph

1. 1 FCLSUM = <E of clauses of Gijll -

(E of clauses of Gi

1.2 FLINKSUM = (E of links of Gi+l) -

(E of links of G. )

1.3 FCANCEL =#{PIP is predicat~ symbol occuring

in Gi+d

1.4 FTERMINATE: (see below)

2. Complexity of the Resolvent

2.1 FAGE =Age of Res

2.2 FLITSUM = Sum of literals in Res

2.3 FTERM = Term complexity of Res

2.4 FRESISO = Degree of isolation of Res

3. Complexity of the Parents of Res

3.1 FPARISO = Degree of isolation of the parents

These features influence the actual derivation in the following way: all steps that lead to a reduc­ tion in the size of the graph have absolute prio­ rity and are immediately executed. That is, every link which leads to a graph with fewer clauses or fewer links or both is put into a special class, which is executed before any further evaluation ta­ kes place. The decision whether or not a link leads to a reduction is based on information from the De­ letion-Module and is optionally taken for every link or for the acUve links only. Note that there­ duction in the size of the graph may lead to further deletions, hence a potential snowball effect of de­ letions is carr-ied out irrmediately, which accounts for the first main source of the strength of the system.

All other features have a relative priority and are classified as situation dependent and situation in­ dependent respectively, since the cost of theirini ­ tial computation and later updating differs funda­ mentally (SS80].

A successful usage of the relative priorities de­ pends on an appropriate metric for each feature, which expresses its estimated worth. A discussion of why the following metrics where chosen is ouande of the scope of this paper and may be found in [SS80]; but the important point to notice is, that each metric displays a particular characteristic, which expresses the heuristic worth relative to its argument.

Age : max{Age Parent1, Age Parent2}+1

D : user defined maximally admitted depth of de­ max rivation

This feature is mainly used to avoid "infinite holes" in the search space.

This feature adds a strong "unit-preference-be­ haviour" to the system.

where: s . :maximal nesting of ith term in Res s ~:user defined maximally admitted depth of max nesting n:number of terms in Res

Note that the value is either 0 or 1 and this infor­ mation is useful for a simulation of Colmerauer's cancellation strategy [K075].

FLINKSUM: has either absolute priority if it decrea­ ses or else is entered into the selection process of the CO-Module with the window­ technique

FRESISO: has either absolute priority if Res is pure, else

FPARISO: similar to FRESISO

Note that FPARISO and FRESISO are useful, since they provide the Control-Module with the information that after one (or less useful, after two) further steps another deletion process starts, which potentially leads again t6 a snowball effect of deletions.

The main constraint for these heuristics is that after each resolution step the values of the heu­ ristic features have to be updated and it is essen­ tial that the cost of this updating is much less than the cost of performing every possible resolu­ tion . For that reason not every value of the argu­ ments for the metrics is computed exactly but esti­ mated by some heuristic estimation function.

The Terminator ModuZe is used in two ways: First it acts like a simple (and relatively fast) theorem prover and is activated on the initial connection graph. If it fails, the full machinery of the logic engine is loaded.

Secondly it is used to overcome the problem that the above heuristics have the very limited horizon of one step ahead, since the computation of a further n-level look ahead for n~2, is so prohibitively ex­ pensive that it outweighs the advantage. For that reason we implemented in addition a different n-le­ vel look ahead technique, which checks at tolerable cost if there is a proof within a predefined com­ plexity bound. This terminator heuristic FTERMINATE is the no-loop-requirement of [SI76, p. 832] and is akin to the n-level-look-ahead heuristic proposed by [K075, p. 593] and is the second main source for the success of the current system. The essential idea is an elaboration of the followingobservation:

Each box in figure 4 represents a literal, a string of boxes is a clause and complementary boxes (li­ terals) are connected by a link. If all unifiers attached to the links in figure 4a are compatible it represents a one-level-terminator, since it imme­ diately allows for the derivation of the empty clause. Similarly figure 4b represents a two-level­ terminator if the unifiers are compatible (see [SSBO] for a detailed presentation). At regular in­ tervals (e.g. after n derivation steps) the Termi­ nator Module searches for such configurations.

2.3 Searching for a Proof

Once the Logic Engine is set into "prove-mode", the CSS-ModuZe converts the activated part of the Data Bank into Skolemized clausal normal form and per­ forms various splitting and truth functional simpli­ fication tasks. The resulting set of clauses is passed on to the CG-Modu"le, which constructs the connection graph and if possible performs an eva­ luation of terms, reductions or algebraic simplifi­ cations of terms with the aid of the above modules. After these activities the initiaZ connectiongraph is set up and now the search for a proof within this graph ccmmences.

This search is locally controlled by the ControZ­ MOduZe, which decides which link to resolve upon next, based on nformation provided by the Heuristic­ Module, the Refinement-Module, the Deletion-Module etc. The Control-Module turns the initial representation of clauses (the connection graph) into a proof procedure (based on connection graphs) as it defines a particular selection function, which maps graphs to links. This mapping is complex and based on information provided by several modules, but for clarity it is entirely contained in the Control-Mo­ dule.

It should not be necessary to say that the complex interplay of the various modules, which 'suggest' which step to take next, prevents of course the overall deduction from being 'standard' and the res­ pective completeness results do not necessarily hold. However, by an appropriate setting of the weight for FAGE, it is impossible for a link to be ignored indefinitely for selection and for that reason we believe the system is complete.

The potential explosion of links is the bottleneck of the connection graph: the following 'challenge' proposed by P. Andrews, Carnegie Mellon at the 1979 Deduction Workshop, provides a point of demonstration: (3x Qx · Vy Qy) · (3x Vy Qx · Qy).

The initial graph of this formula consists of al­ most 10 000 Links and several hundred new links are added to the grpah for each resolution step. If all these links were declared 'active', the computation of the selection functions would become intolerably expensive.

In our system the example is split, reduced and sub­ sequently deleted to a graph never exceeding 50 links and easily proved within a few steps. Even for more 'natural' examples, the number of deletion steps is about one third and sometimes over onehalf of the total number of steps.

Same TechnicaL Data about the Project

Name of Project: Incorporation of Mathematical Knowledge into an ATP-System, in­ vestigated for the case of Auto­ mata Theory.

Funding Agency: German Research Organisation (DFG)

Bonn, De 238/1, De 238/2.

Time Period:

1976 to 1982 (six years)

Machine:

SIEMENS 7. 760

MinimaLly Required Storage Space: 6.000 K (virtual

memory)

SIEMENS-INTERLISP [EP75)

Languages:

of system: ~ 500 K of source code Present size

Effort:

~ 10 manyears for its implement~on

With more than 500 K of actual code at present and approximatly 1.000 K under design for the next two years, the system is the largest software develop­ men t undertaken in the history of automated theorem proving and it may be indicative for the changing pattern of research in this field.

3. PERFORMANCE STATISTICS

To gain a feeling for the improvement achieved by the system, figure 5 gives a sample of some test r uns . In order to avoid one of the pitfalls of sta­ tistical data, which is to show the improvement ach i eved on certain examples and not showing the deter i oration on others, the system is to be tested on all of the main examples quoted in the ATP li­ t erature: [WM76], [MOW76], [RRYKU72]. Of all exanples tested thus far, the examples of figure 5 are re­ presentative (and worstcase, i.e. all other examples were even more favourable for our system). The examples of figure 5 are taken from the extensive, comparative study undertaken at University of Mary­ land [WM76], where eight different proof procedures were tested and statistically evaluated on a total of 152 examples.

The table is to be understood as follows : the first column gives the name of the set of axioms in [WM76], e.g. LS-35 in line 9. The next threecolumns quote the findings of [WM76], where the figure in brackets gives the value for the worst proof pro­ cedure among the eight tested procedures and the other figure gives the value for the proof proce­ dure that performed best. The final three columns give the corresponding values for the Markgraf Karl Procedure. For example, in order to prove the axiom set LS-35 (line 9) the best proof procedure of [WM76] had to generate 335 clauses in order to find the proof, which consisted of 14 clauses, and the worst proof procedure had to generate 1.521 clauses in order to find that proof. In contrast our system generated only 9 clauses and as these figures are typical and hold uniformly for all cases, they are the statistical expression and justification for the first two claims put forward in the abstract.

4. KINSHIP TO OTHER DEDUCTION SYSTEMS

The advent of PLANNER [HE72] marked an important point in the history of automatic theorem proving research [AH72], and although none of the techni­ ques proposed there are actually present in our system it is none the less the product of theshift of the research paradigm, of which PLANNER was an early hallmark.

The work most influential, which more permeatesour system than is possible to credit in detail, is that of W. Bledsoe, University of Texas [BT75], [BB75], [BB72), [BL71), [BL77). In contrast to [BT75], we tried to separate as much as possible the logic within which the proofs are carried out from the heuristics which are helpful in finding the proof.

The strongest resolution based system at presentis [MOW76], and we have tested their examples in our system. Comparison with their reported results, shows that if our system finds a proof it is su­ perior to the same degree as reported in figure 5.

However, there are still several more difficult examples reported in [MOW76] which we can not prove at present. The strength of the system [MOW76] de­ rives mainly from a successful technique to handle equality axioms and almost all the examples quoted in [MOW76] rely on this technique. For that reason, as long as our paramodulation module is not fully equipped with proper heuristics there is no fair comparison (the test cases were obtained with the full set of equality axioms and no special treat­ ment for the equality predicate).

Finally among the very large systems which present­ ly dominate theorem proving research is the system developed by R. Boyer and J.S. Moore at SRI [BM78]. Their system relies on powerful induction techni­ ques and although some of the easier examples quo­ ted in [BM78] could be proved by our system at pre­ sent, a justifiable comparison is only possible once our induction modules are completed .

A theorem prover based on heuristic evaluation was also reported by Slagle and Farrell [SF71] however it appears that such heuristics are not too success­ ful for an ordinary resolution based prover.

5. CONCLUSION

At present the system performs substantially better than most other automatic theorem proving systems, however on certain classes of examples (induction, equality) the comparison is unfavourable for our system (section 4). But there is litt1e doubt that these shortcomings reflect the present state of de­ velopment; once the other modules (T-unification, paramodulated connection graphs, a far more refined monitoring, induction, improved heuristics etc) are operational, traditional theorem provers will no longer be competitive.

This statement is less comforting than it appea{S: the comparison is based on measures of the search space and it totaZZy negZects the (enormous) re­ sources needed in order to achieve the behaviour described. Within this frame of reference it would be easy to design the "perfect" proof procedure: the supervisor and the look-ahead heuristics would find the proof and then guide the system without any unnecessary steps through the search space.

Doubtlessy, the TP systems of the future will have to be evaluated in totally different terms, which take into account the totaZ (time and space) re­ sources needed in order to find the proof of a given theorem.

In summary, although there are good fundamental ar­ guments supporting the hypothesis that the future of TP research is with the finely knowledge enginee­ red systems as proposed here, there is at present no evidence that a traditional TP with its capacity to quickly generate many ten thousands of clauses is not just as capable. The situation is reminiscent of todays chess playing programs, where the pro­ grams based on intellectually more interesting prin­ ciples are outperformed by the brute force systems relying on advances in hardware technology.