Bruno Buchberger, Tudor Jebelean, Daniela Vasaru
Research Institute for Symbolic Computation
A-4232 Schloss Hagenberg, Austria
last-name@risc.uni-linz.ac.at
23 October 1997
Lack of formal training is hindering the application of high-level information technology in science and engineering. The Theorema project addresses this need by implementing a sophisticated automatic reasoning system with an easy-to-use interface which can be used in various interactive ways - both locally and over the internet. In contrast with most of the theorem proving systems, the Theorema software presents its results in natural language and also develops proofs in human style. We report on the use of this software for the training of mathematics and engineering students in problem solving and in theorem proving.
This document is better viewed as Mathematica notebook. If you do not have an installation of Mathematica 3.0, then you can download MathReader free of charge.
We provide in this section some examples of proofs produced by various provers: the predicate logic prover, the prover by induction on natural numbers and the prover by induction on lists. All the proofs have been produced completely automatically, including the natural language text and the nested cell structure, except the proof in analysis - which was produced in active mode with control from the user.