RISC
Institute HagenbergRISC
Institute HagenbergThe following description is a snapshot from February 2002. For up-to-date information on the Theorema project, we refer to the Theorema website.
In the year 2001, various strong components have been built into Theorema on the foundations laid in the previous years of the project. One of them is the set-theory prover of Theorema, an implementation of special inference rules for set theory, corresponding to various reasoning steps used by the working mathematician in a typical informal proof. The technique is based on the PCS proving method, see below. Since set theory is at the heart of mathematics (e.g. all the volumes of the monumental Bourbaki oeuvre are based on a version of Zermelo-Fraenkel set theory), this gives the user a powerful proving tool. [8]
Another important component developed intensively in 2001 is the geometry prover of Theorema. Geometric theorem proving is a very traditional - maybe even an original - branch of mathematics, going back to the ancient school of Euclid. It is a marvelous fact that all of these classical theorems (and many more) can nowadays be proved by purely algebraic methods like Gröbner bases or the area method. This is in complete accordance with the overall philosophy of Theorema, which emphasizes the importance of combining provers and solvers for obtaining more powerful proving methods. The geometry prover of Theorema provides various such combined methods for deriving a lot of substantial results like Pappus's Theorem.
The general provers of predicate logic have also been enhanced in various ways: First, there is a new meta-strategy called ``S-decomposition'' for obtaining very natural proofs of theorems such as the ones typically encountered in elementary analysis. The main idea is to introduce Skolem constants and meta-variables in goal and assumptions in various parallel waves. Second, a new natural-style predicate prover has been developed for a sound treatment of meta-variables and deferred proof obligations. [3, 4]
Third, the PCS proving strategy (basically a predicate-logic prover that is skilfully enhanced by a special solver over the reals has been improved. The rewrite prover, an essential building block for many proof problems, has been rewritten completely. Among other features, it provides a Knuth-Bendix completion procedure and a unification algorithm for sequence variables. The theory of sequence unification is a very young research topic which is also advanced by the Theorema project. It has a powerful impact on formalizing and proving theorems e.g. about arithmetic operators in a natural way. [2, 5]
Besides these prover modules, the system environment has been extended in several directions. The so-called focus windows are a novel method, proposed by B. Buchberger, for advanced proof presentation : The user sees the whole proof like a movie in a series of snapshots, each of them specifying one proof situation, where the relevant assumptions are filtered out from the knowledge base and the current inference step is described. The advantage of this presentation style is that a reader is not distracted by dozens of irrelevant assumptions, and the mind becomes free to concentrate on the essential parts; this is of great help especially for understanding complicated proofs. [7]
Another new feature is the interactive interface to provers. In the community of automated-theorem proving, there are two main interest groups: one for proof search, the other for proof verification. All the provers described up to now are fully automated, thus giving the user maximum computer support by doing the whole proof search. On the other hand, it is often desirable to interact in certain critical moments, e.g. by providing witness terms in an existential subgoal; this is now possible for Theorema provers. Since one can still delegate the ``routine parts'' of a proof to the machine, this seems to be an optimal compromise between full proof search and mere proof verification.
A novel approach to advanced logical syntax is realized by so-called logico-graphical symbols. They combine the indispensible quality of mathematical rigor with the intuitive power of well-chosen graphical symbols. In Theorema, it is now possible to use any self-created symbol or even arbitrary Postscript images for denoting function symbols, predicate symbols, object constants or special quantifiers. This opens new possibilities for displaying proofs that are as easy to read as possible, while still having the full logical precision of traditional proofs. [1]
Besides all these internal components of Theorema, there are also numerous interfaces to external proof engines; the current list runs as follows: Otter, Gandalf, Waldmeister, Spass, Bliksem, Vampire, E, Setheo, Scott, EQP, Mace. Hence one can formulate a complicated theorem once in Theorema and then call the various proof engines on them without leaving Theorema. Since each of these engines has its own strengths and weaknesses, it can be very benificial to go over this interface. They can also be combined with other Theorema provers or amongst themselves for gaining special efficiency. An example described in the above paper is the combination of the first-order prover Otter with the counter-model searcher Mace: started on some formula (and we do not know whether it is true or false), Otter will attempt to prove it; if this fails, Mace is started for searching a couter-example. [6]