Theory of "Groebner Bases'' / The Theorema Project / Decomposition of Goedel Numberings / Computer-Trees and the L-Machine / P-adic Arithmetic / Hybrid Approach to Robotics / Systolic Algorithms for Computer Algebra

Main Contributions / The Theorema Project

The Theorema project is also a part of the SFB (Special Research Consortium) "Scientific Computing" at the University of Linz, sponsored by the FWF (Austrian National Science Foundation).

The Theorema Project is my main research interest since 1995. However, basically, all my previous math activities can be view as preparatory work to the Theorema Project: In an oversimplified view, the objective of the Theorema project is the development of a software system that simulates my own proof methods and proof style which I apply in research and I also teach as a part of my "Thinking, Speaking, Writing" course. More generally, the Theorema software system is a uniform logic and software technologic frame for supporting all phases of the mathematical exploration cycle: formalization, proving, solving, computing. The system is programmed in Mathematica and consists of the following parts:

• a syntax analyzer that accepts two-dimensional mathematical formulae in a notation that is very close to the "usual" mathematical notation in textbooks,
• a mechanism for expressing functors,
• a formal language that allows to build up hierarchies of labeled formulae in structured mathematical knowledge bases,
• various general and special provers for the automated generation of proofs for various classes of mathematical formulae (e.g. general predicate logic formulae, equalities over natural numbers and other inductive domains, boolean combinations of equalities over the complex numbers, set theory formulae, etc.),
• post-processors that present the proofs generated in various natural languages (at the moment English and Japanese),
• interfaces for sending formulae and knowledge bases from Theorema to various external provers like Otter etc. and for translating the output of these provers back to Theorema syntax,
• a mechanism for accessing all Mathematica functions from within Theorema.

Recently I introduced the notion of "logicographic" symbols that open new possibilities for combining formal reasoning with graphical intuition.