RISC-Linz RISC-Linz Research Institute for Symbolic Computation  

Theorema 1.x (outdated version)

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

Version Info

Theorema 1.x can be downloaded from this page (see below), but please be aware that this version of the software is outdated and will not be supported anymore. Please note that Theorema 1.x does not run under Mathematica 8, so you need Mathematica 7 or older to run this version of Theorema.

Theorema is currently being re-implemented under the name Theorema 2.0. The new release will be available as source code under GPL license soon, for more details go to this page.

The rest of this page is from the old web pages ...

Example Proofs Generated by Theorema

Theorema on the Web

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:

Privacy Statement
We record your data, in particular your email address, only to inform you on new developments of the Theorema software.
By downloading the Theorema software you agree to receive email on that matter in the future.
We will not forward any of your personal data to third parties or use it for other purposes than described on these pages.

Maintained by Webmaster.
© Research Institute for Symbolic Computation.