PROVE

In the frame of the Theorema project a software system is developed on the basis Mathematica that supports the automated generation of mathematical proofs. The emphasis lies on producing proofs in a style that comes close to the style in which human mathematicians write down their proofs. At the same time, an input language based on usual predicate logic is being developed, which also allows input in a form like mathematicians are used to from scientific publishing. General prove techniques that have their application in virtually all fields of mathematics must be provided by the system, such as propositional logic proving, predicate logic proving, set theory proving, proving with case distinctions, induction over various domains, etc. Moreover, the system must be well designed from a usability point of view, because otherwise potential users cannot be encouraged to use the system. Thus, this part of the Theorema project deals with user interface design, general system engineering for keeping the system maintainable as it is steadily growing, and improvement of general methods that are not tailored for particular areas of mathematics.