Mathematical Knowldge Management and 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 presentation will be structured as follows:
- 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.