The Theorema System

Theorema: A System for Computer Supported Mathematical Theorem Proving and Theory Exploration

Example Proofs Generated by Theorema

Example Computations for Boundary Problems in Theorema

The Theorema language allows to integrate computations (“programming”) along with mathematical theorem proving as another crucial ingredient of theory exploration. As an example, we have coded an operator-based algorithm for computing Green's operators for linear boundary problems (both ODEs and simple PDEs) directly in a Theorema notebook. Our approach relies on a noncommutative Gröbner basis that describes the relations of the basic analysis operators appearing in boundary problems; see our article for details.

Example Computations for Integro-Differential Polynomials in Theorema

A prototype implementation along with some example computations for the integro-differential polynomials modeling non-linear differential and integral expressions containing indeterminate functions can be found in the following Mathematica notebook. We also provide an automated proof for the confluence of a rewrite system for integro-differential operators corresponding to an infinitely generated noncommutative polynomial ideal, to be found in this Mathematica notebook. If you do not have an installation of Mathematica, please have a look at the code and the proof PDFs instead.

System Information

Theorema is based on Mathematica and is working on all machines that support Mathematica. Mathematica version 4.0 or later is needed in order to run the Theorema system. The latest version Theorema 1.6alpha also runs with Mathematica 6.0.

Download Theorema

Downloading the Theorema system is free of charge!
Please complete the following form and press the "Next >" button below in order to proceed to the download area: