Solving and Proving in General Domains - Period I (Subproject of SFB F 13 Numerical and Symbolic Scientific Computation)

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. For the next three years, the emphasis in this part of the Theorema endeavour has been put on a cooperation with a project group from the institute for industrial mathematics led by Prof. H. Engl for using the Theorema system for generating automated proofs in the theory of Hilbert spaces, which is one of the theoretical foundations for Regularization theory, which is in the focus of interest of research in the field of numerical mathematics.