Theorema 2.0: A System for Mathematical Theory Exploration

Theorema 2.0 stands for a re-design including a complete 
re-implementation of the Theorema system, which was originally 
designed, developed, and implemented by Bruno Buchberger and his Theorema
group at RISC. In this talk, we want to present the current status of the
new implementation.

The emphasis of this presentation is on the user interface of the system,
i.e. how a user is supposed to get her jobs done supported by the Theorema 
system. Topics range from formula input over structuring and administration
of bigger knowledge bases, knowledge archives, automated proving, interactive
proving, customization of automated proving methods, generation of
readable proofs until tool support for navigating through large structured
proofs.

Theorema 2.0 is - like its predecessor versions - based on Mathematica, which
means that it is implemented in the Mathematica programming language and that
it uses the Mathematica notebook frontend as its user interface. Unlike the
command-oriented interaction pattern typically propagated in Mathematica
applications, Theorema 2.0 is heavily based on the graphical user interface
capabilities supported in recent versions of Mathematica. As a result, the
user needs the keyboard only for typing the mathematics (definitions, theorems,
explanatory text) into the system, all actions to be performed are guided by
the graphical user interface. Following this approach, the difference between
writing a Theorema document and writing a "standard mathematical document"
shrinks to almost zero. Moreover, the learning curve for using a mathematical
assistant system is considerably flattened and the system will be more
attractive, in particular for beginners. 

Theorema 2.0 runs on all platforms, on which Mathematica is available.
Mathematica is needed to run the system, but the Theorema system itself is
open source licensed under GPL and is available at GitHub.

The talk is intended as a live system demo and should serve as an introductory
course for other workshop presentations related to the Theorema system.