
Theory of "Groebner
Bases'' / The
Theorema Project / Decomposition
of Goedel Numberings / ComputerTrees
and the LMachine / Padic
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 twodimensional 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.),
 postprocessors 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.

