# Theorema:

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

*last-name*@risc.uni-linz.ac.at

23 October 1997

#### Abstract

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

### Examples

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

#### Lists

### References