Compilation of Theorema Programs

n this thesis we present a compiler which is able to translate Theorema programs into executable Java code, which can then be used for extensive and fast calculations called from within Theorema. Generally, it can be observed that higher elegance in programming languages and software systems must be paid for by dramatically increasing computing times, see for example Prolog computations and original Theorema. One of the basic strategical goals of the Theorema system is to offer predicate logic as a uniform frame for the three main activities of mathematics: proving, solving, and computing. It is one of the strong features of Theorema that it combines automated theorem proving and computation in one logical and software frame. In fact, the same Theorema definitions that are used for stating and proving theorems can also be applied for computing. The actual motivation for this thesis was the slowness of computations in the current version of Theorema, which is due to the usage of special logical inference rules (directed equational logic) as an interpreter for the Theorema algorithms. Therefore, it is of utmost importance to ...