Exploring Computer Mathematics with Theorema
The Theorema system is developed at RISC-Linz by the
Theorema group, under the leadership of Bruno Buchberger.
The goal of the Theorema project is to provide computer support for all phases
of the mathematical work: to prove theorems, use them for computations and
experiments, conjecture new theorems, prove those, extract solution methods
from them, apply them in other proofs, etc.
The Theorema system
offers these features in one coherent software package which is currently based
on the rewrite engine of the computer algebra system Mathematica.
The particular features of the system include:
- a simple an intuitive set of commands for writing, structuring, and using
mathematical knowledge (MK) for proving, computing, and solving;
- the use of higher-order predicate logic as the natural language for
expressing mathematical formulae:
that means both mathematical assertions (as definitions, axioms, theorems),
as well as algorithms ("programs");
- a collection of provers for general logic as well as for specific
domains (set theory, tuples, natural numbers, elementary analysis);
- the use of natural language for expressing MK (that is traditional
2D notation for formulae, as well as natural language explanation of proofs),
as well as the use of natural style proving (that is natural inference steps,
human-like).
The tutorial will contain 4 parts of about 30 minutes each:
- Overview of the system:
- the basic concept explained through a simple example;
- the user interface;
- the system architecture;
- overview of the provers.
- Some methods for proving in natural style:
- combining prove/compute/solve in one method: PCS proving of limit theorems;
- extending PCS to set theory;
- organizing logic inferences by S-Decomposition: limit theorems revisited;
- induction extended by automatic conjecturing: inventing lemmatas in natural number theory.
- MK management, programming, computing, and proving: the tuples
- constructing the theory of tuples by "lazy" exploration;
- predicate logic with equality as programming language: sorting;
- computing: experiments with the sorting algorithm;
- proving algorithm correctness.
- Future developments in Theorema:
- building your own provers: a language for describing inferences and their combinations;
- program verification: functional versus imperative;
- program synthesis: a practical approach;
- the importance of MK management and retrieval;
- advanced proof presentation: focus windows, interactivity.
The presentation will be based on concrete live experiments with the
Theorema system, with concrete examples from various elementary theories.
The audience is not expected to have specific training in any
particular area, let it be automatic reasoning, computer algebra, or program
verification. A general graduate level of knowledge in mathematics and
computer science should suffice, since the Theorema system addresses all
mathematicians, computer scientists, and engineers.
Throughout the presentation, we will give particular emphasis to refining
and explaining the research problems described in the companion document
Research problems related to Theorema.
The support of the presentation will be distributed to the tutorial
attendees in electronic format, together with a working copy of the Theorema
system (machine code, 12 months user license).
Interested participants will be invited to become alpha-testers of Theorema.