The Theorema system is developed at RISC-Linz by the Theorema group, under the leadership of Bruno Buchberger. This document is companion to the abstract of the tutorial Exploring Computer Mathematics with Theorema.
A proof in presentation style will continue with: "We prove now that the limit of f+g is a+b." The prover guesses (like by magic) which is the appropriate limit, and later in this proof it will also guess good terms like e/2, max(M,N), in the same magic way. In fact, these terms can be discovered only by performing the proof by some other method. However the proof is enough to convince somebody about the truth of the sentence.
A proof in discovering style will (in contrast) continue with: "We must find a value c which is the limit of f+g." The second prover will later introduce more such "must find" variables, which are names for terms which we do not know yet, and at certain moments in the proof it will figure out which are the appropriate values of these unknowns. This proof is also convincing, although a bit more difficult to follow, however it also shows the reader how to find the appropriate terms. (The reader may later use similar techniques in other proofs.)
These temporary unknowns are usually called "meta-variables", and they occur in natural style proofs and also in tableaux methods. The research problem is to find efficient methods/strategies for combining inference rules which introduce/solve meta-variables with other natural style inference rules, such that the proofs obtained are natural and compact. The problem is relevant both for provers in general logic as well as for provers in specific domains - which suggests that it may be possible to find strategies which are valid for any set of inference rules. The experiments we did in the frame of the Theorema project show that a straightforward adaptation of the techniques used in tableaux proving leads to inefficient methods (large search space) and unnatural proofs (wrong order of inference steps). On the other hand, certain specific strategies can be both efficient and natural for certain types of problems (e.g. S-decomposition for limit theorems).
Moreover, in the Theorema project we noticed that sequence variables are very useful for natural expression of many mathematical statements, especially in the domain of tuples. A sequence variable is a symbol which stands for the occurrence of an arbitrary number of terms (in contrast to a normal variable which stands for the occurrence of a single term). For instance, if x is a usual variable and X is a sequence variable, then the term [x, X] stands for [x1], for [x1, x2], for [x1, x2, x3], etc., thus for any tuple with at least one element. One may then write definitions like: "For any x, y and any sequence Z, the list [x, y, Z] is sorted if and only if x is greater than y and [y, Z] is sorted."
The research problem consists in finding efficient strategies for equality reasoning in the context of natural style proving (possibly also by adapting Knuth-Bendix completion and paramodulation), and to adapt these techniques, and/or invent others, for the formulae which contain sequence variables.
Even when the media is very interactive (ideally the Theorema system), sometimes the user only needs to follow the finished proof, sometimes he also needs to interact with the proof in order to develop it. For the former situation we experimented with the technique of focus windows, which shows only the relevant formulae at each step, for the later we are developing an interactive frame, which allows navigation and controlled expansion of the proof tree.
The research problem consists in finding and implementing the most appropriate presentation techniques for different concrete situations. This also includes experimentation with [numerous] concrete users, and has a certain impact on the overall design of the system: for instance, the information provided by various provers has to be standardized such that it can be used by any presentation engine.
Throughout the tutorial, we will give particular emphasis to refining and explaining the research problems described above.