A System for Formal Scientific Training
in Natural Language Presentation

Bruno Buchberger, Tudor Jebelean, Daniela Vasaru
Research Institute for Symbolic Computation
A-4232 Schloss Hagenberg, Austria

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.

Background and Motivation

The Theorema Project

Using Theorema for Proof Training


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.

Predicate Logic

Natural Numbers