Around 1990 the work on the first-order theorem prover MKRP stopped after a development going on for more than a decade. Instead a new system has been developed since then, the mathematical assistant Omega . In this contribution I try to summarise some of the discussions and decisions that led to this shift in focus and to the development of the Omega system, and I attempt in retrospect to give a tentative evaluation of some of the decisions.
The MKRP -project started in Karlsruhe when Jörg Siekmann was a research fellow at the University of Karlsruhe and was continued when he took up there a professorship for artificial intelligence at the University of Kaiserslautern. In this paper some details about MKRP and the MKRP -project are discussed, but only insofar as they are relevant for the transition from MKRP to Omega . It is not a description of the development of MKRP (neither of Omega ), but a report on the transition period.
In order to understand the transition let's first take a look at the context in which the decisions were made, then take a closer look at the MKRP system itself and discuss shortcomings of the system in the intended applications and means to overcome these.
MKRP was built on the so-called clause graph procedure, originally proposed by Robert Kowalski [Kowalski75]. In this approach, a graph is used to store all possible resolution steps, detect redundancies and simplification possibilities. A difficult question is whether the procedure is actually complete and confluent, that is, whether if one starts with an unsatisfiable clause set, from any intermediate state it is still possible to derive the empty clause, and - assumed a fair strategy is employed - the empty clause will eventually be derived.
Norbert Eisinger [Eisinger91] studied the theoretical properties of clause graph procedure like completeness and confluence. Already during the Karlsruhe phase, Christoph Walther [Walther83] developed the order-sorted logicThe idea of sorts is to replace particular unary predicate symbols by sort symbols. This has the advantage to shorten clauses and prevent meaningless unifications. on which MKRP is based. In Kaiserslautern, Manfred Schmidt-Schau\ss [Schmidt89] worked on extensions of this logic with term declarations. Hans-Jürgen Bürckert [Buerckert90] worked on constraint resolution, Alexander Herold [HeroldPhD] on the combination of unification algorithms, and Christoph Lingenfelder [Lingenfelder90] on the presentation of resolution proof in natural deduction. Karl Hans Bläsius [Blaesius86] and Axel Präcklein [Praecklein92a] worked on different approaches to equality reasoning from human-oriented to traditional rewrite oriented ones. Hans Jürgen Ohlbach (but also many others) were very involved in the MKRP project or related projects. They played a crucial role in the development of MKRP and of extensions to MKRP . Hans Jürgen in the end chose a PhD topic on modal logic rather than MKRP -related issues [OhlbachPhD].
While all these people finished their PhDs, two things crucial for the further development happened around the same time, firstly the German Research Centre for Artificial Intelligence (Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI) was founded in Saarbrücken and Kaiserslautern, and secondly Jörg Siekmann was offered and accepted a full professorship (C4) in Saarbrücken, jointly with the post of a director at the DFKI. This meant not only that a shift in the focus of his work was necessary, but also that senior people were needed to head the new research areas in the DFKI.
Initially, the Omega -group (in addition to Jörg Siekmann himself) consisted of Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Erica Melis, Dan Nesmith, and Jörn Richts. While Xiaorong and Manfred had worked in the group for a couple of years already, Xiaorong on the verbalisation of natural deduction proofs, and Manfred on human-oriented theorem proving, the others recently joined. Michael had just met Jörg Siekmann at a seminar of the prestigious Studienstiftung. His special interest was to develop a logic close to the mathematical representation found in mathematical practice, concretely this meant to develop a sorted higher-order logic and its mechanisation. Erica had worked on analogy and related questions in a general context at the Humboldt University in Berlin; she joined the group after she met Manfred just before the fall of the wall at a conference on analogy in East Germany. Dan came - a short while after the others - from Peter Andrews' group to Saarbrücken. He brought in his tremendous experience in the implementation of the TPS system. This way TPS strongly influenced the style of the logical core of Omega . Dan was to become the main developer of the Keim implementation system, which has provided the implementational base for Omega [Keim94]. Jörn had just finished his master thesis on MKRP and had a general interest in the new paradigm of Omega .
At a time Axel Präcklein built an interactive component as an extension to MKRP which visualised all possible resolution steps and allowed to run MKRP in an interactive mode. Using this component, Axel Präcklein and Manfred Kerber tried to find patterns in the clause graph which allow to select the next resolution possibility heuristically. However, it turned out that it was already very difficult to find proofs at all this way and virtually impossible to detect any usable structure. Usually MKRP performed these steps much better than humans. From this it was concluded that automating a human-oriented selection module for resolution steps would be very difficult (it wouldn't have been very human-oriented anyway).
The motivation force in the MKRP project was to prove a mathematical textbook fully using MKRP . The only ever fully proved mathematical textbook is Edmund Landau's "Grundlagen der Analysis" [Landau30]. This book was interactively proved in the Automath system see [Nederpelt94] by L.S. van Benthem-Jutting [Jutting79]. It was a major attempt to prove a full mathematical textbook and it took van Benthem-Jutting five years to do it, although Landau's book is very formalised with 301 theorems on 134 pages. The effort needed indicates that Automath seems not to have been the right tool to prove textbooks. While it is a proof checker, MKRP is an automated theorem prover. The hope was that this would make it much easier to prove a book with MKRP . The textbook chosen was Peter Deussen's "Halbgruppen und Automaten" (Semi-groups and Automata) [Deussen71]. The first 5 of 17 sections were actually proved with MKRP . As will be seen in the following, there were, however, severe problems with using MKRP for this task. When we formed plans for a new project, Omega , we naturally wanted to take into account all the lessons learned from the attempt to prove the text book. In the following the most important insights will be summarised which strongly influenced the further development (see also [KerberDiss] and [HuKe-etal-SR-92-22]).
Logic The representation of the mathematical concepts in the sorted first-order input language of MKRP is often clumsy and unnatural, also the representation was often ad hoc. The concepts and constructs of a typical mathematics textbook are quite rich and much better approximated by a higher-order language, we were forced to use sophisticated encoding techniques to translate them manually into the MKRP first-order input language. While the availability of sorts and the built-in equality predicate allow for a tolerably adequate translation, it is not always obvious what the theorems proved by MKRP have to do with the textbook theorems and hence what is actually proven. As a minimal requirement one would want an automatic translation technique from higher-order to first-order logic to support a user in the encoding task.
Knowledge Base The MKRP -system, as most other automated theorem provers, has no integrated mathematical knowledge. Each time definitions and lemmas, which are used as preconditions for the actual theorem, must be coded and re-input. This is not only rather boring, but is also a serious source of error. Often (slightly) different formulations are chosen in different contexts, with the consequence that the correctness of the whole procedure of machine verification of textbooks is no longer assured. Moreover, the user may insert lemmas that cannot be proven in the given context. Discipline may be helpful, but as practice shows, automated assistance is indispensable. In short, a system that supports human mathematicians in proving theorems must include a database of mathematical knowledge that can be accessed and updated in a controlled way. This in itself is a major research task, still not fully solved.
Structuring in subproblems More often than not, real mathematical theorems are too hard to be proven automatically. This state of affairs can be ameliorated by strengthening the deductive power of the prover in various ways (and since then considerable progress has been made in the field, of course). For every system, however, there exist theorems that cannot be shown automatically. In order to be useful, the user must be given the opportunity to guide the proof process interactively. In a classical theorem-proving system this is almost impossible: the cycle of interaction consists of a complete restart with a different setting of the parameters or a reformulation of the clauses. The main influence the user has, consists in the appropriate choice and formulation of the problem. The way the preconditions of a theorem are selected, for instance, is of paramount importance for the performance of the system. An additional necessary facility is one for splitting the problem manually into subproblems, so that they can be proved separately and then used as lemmas later in the proof of the original theorem. Traditional theorem provers lack such support and the situation is far from satisfactory, as all structuring decisions and all proof plans are hand-crafted. In short, all of this requires too much care and skill from the user, and not surprisingly there are fewer than a handful of well-known experts who are renowned for their skill in proving difficult theorems with the help of a machine. Since it is always possible to break down difficult theorems into digestible subproblems, there is also the question to which degree this procedure can be called automatic.
All these points showed us that we needed a new system which should be developed from scratch and that there was no point in attempting to extend the existing MKRP system. However, we were also very reluctant to throw away more than ten years of development work and dozens of person years' work. This led to the idea to build an open system, in which it is possible to add external systems to solve subproblems. The first external system would be MKRP , others could then easily follow.
The principles for the Omega system were developed in many meetings, seminars and discussions, a picture of one of the blackboard summaries can be found in Fig. 2. These discussions were influenced by many people, who either came to the group to give presentations or with whom we were in intensive discussions. To mention just a few: Jörg Denzinger (with whom we had intensive discussions on proof planning), Christoph Kreitz (who explained to us the details of Nuprl ), Wolfgang Reif (on the reuse of proof attempts), William Farmer (on the IMPS system). In addition, we had numerous discussions with Dieter Hutter, Claus Sengler, Jürgen Cleve and others, who just arrived in Saarbrücken at the same time as we, to work on Jörg Siekmann 's verification project. Furthermore we read many articles outside the main paradigm of the MKRP system, such as papers on Automath [Bruijn80,Nederpelt94], Isabelle [Paulson90], and proof planning [Bundy88].
These discussions were about almost all aspects of a system, from the high-level philosophy of the system to the implementation language and the data structures employed. In the remainder of this section I want to summarise some key questions and decisions. Let us first take a look at the philosophy of the system. In this we took up the experience gathered in the work of proving the first third of [Deussen71].
A quote from [Omega94]:
On account of this, we believe that significantly more support for
proof development can be provided by a system with the following two
As a consequence we decided to build a system that on the one hand allows for tactical theorem proving, which allows to influence the proof search by calling tactics, and on the other hand has integrated strong external components like automated theorem provers which can be called as black boxes to solve subproblems (see Fig. 3). In summary we tried to find a viable compromise between automatic and interactive theorem proving. In retrospect, the decision to follow an automatic and interactive approach at the same time seems to have been the right one. The full strength of this synthesis seems to be coming to the fore only recently in work on agent-oriented theorem proving as developed by Christoph Benzmüller and Volker Sorge [Benzmueller01:OANTS] and multi initiative proof planning by Andreas Meier and Erica Melis [Meier00].
Related to (but independent from) the question whether to follow an automated or an interactive theorem proving style, was the question what the type of the system should be, should it follow traditional machine-oriented theorem proving or human-oriented theorem proving.
Here again, we followed the approach that we wanted to include different paradigms. We wanted to include theorem provers like MKRP and Otter , but wanted also to take the original idea of a human-oriented approach very seriously (see Fig. 3). Some work on analogical theorem proving [Kerber89-AII] was done at that time. Around the same time we understood the significance of Alan Bundy's approach to use planning techniques in theorem proving in the form of proof planning [Bundy88]. It was at the same time when the last proposal to reimplement MKRP and to bring it up to the most recent developments in resolution style theorem proving was discussed. We decided against this and started concrete work on the Omega system instead. We decided to make use of fast existing first-order theorem provers like Otter rather than to bring MKRP to speed.
The approach of proof planning looked very attractive since it allows - unlike MKRP - to include domain-dependent reasoning knowledge in form of proof planning methods [MelisSiekmann99]. Around this time we also adopted the idea that for automation incomplete approaches can be stronger than complete ones.
The overall architecture of Omega as discussed then and realised later can be seen in Fig. 4. Centred around the structure of Natural Deduction proofs, different components and the user can manipulate partial proofs to complete a proof, this can be done by inserting information from a knowledge base, by proof planning, by external components, or proof transformation.
The argument was strongly supported by the plan to build on existing sort systems (like that used in MKRP ) to extend it to higher-order logic, so that it would be possible to speak about unary functions on real numbers, continuous, and differentiable ones and so on. Here two different aspects had to be considered. Firstly we wanted to use the language as the representation language, that is, we wanted it to be as strong as possible (including dependent sorts, to be able to encode structures like groups very naturally as a set G:set with an operation +:G x G-> G, where the operation depends on G). Secondly Michael Kohlhase wanted to (and later did in collaboration with Christoph Benzmüller) build a theorem prover based on higher-order logic with sorts which should form the Logic Engine for Omega, Leo [KohlhaseDiss,Benzmueller98:LEO]. Since this is a very difficult task, dependent sorts (as well as partiality as discussed in [KeKo96-KGS]) were not included for the time being.
The importance of an adequate presentation of proofs has always played a significant role in the MKRP as well as the Omega project. This started by the work of Christoph Lingenfelder [Lingenfelder89,Lingenfelder90,Lingenfelder91] and Xiaorong Huang [Huang96] and has been continued by Armin Fiedler since. From the work to present proofs to humans it was a short step to arrive at the philosophical position that proofs must be checkable [HuKe-etal94-CADE-WS-Meta]. This solved a major problem of the structure of the Omega system, namely, how is it possible to ensure correctness of proofs in the presence of many - quite heterogeneous black box components - which may contribute to a proof.
The Omega system went first with an Emacs interface only. In the initial discussions we discussed already the importance of a high-level user interface, but in the implementation we had to focus on the kernel of the system. Only later LOUI [Loui99] was developed to provide a graphical user interface to Omega .
Omega was not directly implemented in Lisp (Common-Lisp to be more precise), but in the Keim environment, which was a programming environment built on top of Lisp (in the German Focal Programme on Deduction, financed by the Deutsche Forschungsgemeinschaft). Its philosophy is (quote from [Keim94]):
|..., those who wish to apply techniques developed by the theorem-proving community face the choice of either learning this `black art' themselves by developing their own prover from scratch, or jury-rigging available provers to get some kind of result.|
While Keim greatly facilitated the development of Omega , it remained still a `black art' to build and extend Omega . Keim turned out to be a complex system, which is difficult to handle. Furthermore there are performance problems. In retrospect I think these are due to the attempt to build with Keim a system which is very general and construed to enable the implementation of a wide range of deduction systems. The question whether to build a system as general as possible versus to build a system as simple as possible was answered in favour of generality. This seems to me now to have been a mistake.
There are developments we did not anticipate, but which were made possible by Omega . I want to mention agent-oriented theorem proving [Benzmueller01:OANTS], knowledge-based proof planning [MelisSiekmann99], Mathweb [FraKoh:mabdl99], and OMDoc [Kohlhase:otisadt00]. In my view this shows that Omega has been a flourishing project.
Omega meant a change of direction in Jörg Siekmann 's theorem proving group, a change in area, in approach, and in paradigm. This was of course very risky, since it meant a reduced possibility for publications for a significant amount of time and the potential knock-on effect on funding. Fortunately referees in the German funding organisations were very positive and supportive (I just want to mention Wolfgang Bibel and Michael M. Richter here). I think that Omega has been a scientific success and a worthwhile enterprise. Jörg Siekmann was already an established scientist who could have rested on his laurels and continued with what he always did, when Omega started. He, however, actively initiated this major change in direction, which considerably deviated from the path originally envisaged in the MKRP project, when he was convinced that only in this way we would come closer to making the old dream true to automate mathematics. Leibniz had a dream, "Calculemus", namely to mechanise mathematics (actually he wanted to mechanise not only mathematics but all of human thought, we never were so ambitious in the Omega project). There are many problems in detail still to be solved to provide a powerful useful tool for mechanised mathematics. In the past there have been too many promises/predictions about what will be achieved in the near future. I don't want to add another one, but although we have not yet realised the dream, I feel that we are significantly closer to its realisation.
This paper is not a survey on the Omega system, but just on the discussions during the transition from MKRP to Omega . Many exciting developments have taken place since then and without doubt will take place in the future. They have to be reported somewhere else.
I feel that the description which I tried to provide here is more incoherent and subjective than I would like it to be; this is entirely my fault. That it is not even more incoherent is due to many helpful comments by Norbert Eisinger, Michael Kohlhase, and Erica Melis on a earlier draft. I would like to express my thanks to them hereby.