Solving and Proving in General Domains - Period I (Subproject of SFB F 13 Numerical and Symbolic Scientific Computation)
Sprache der Bezeichnung:
Englisch
Original Kurzfassung:
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.
Forschungs-