@inproceedings{RISC5516,author = {W. Windsteiger},
title = {{Theorema 2.0: A Brief Tutorial}},
booktitle = {{Proceedings of SYNASC 2017}},
language = {english},
abstract = {The Theorema system aims to be a computer assistant for the
working mathematician. Support should be given throughout all phases of
mathematical activity, from introducing new mathematical concepts by
definitions or axioms, through first (computational) experiments, the
formulation of theorems, their justification by an exact proof, the
application of a theorem as an algorithm, to the dissemination of the
results in form of a mathematical publication, the build up of bigger
libraries of certified mathematical content and the like. One focus lies
on the natural style of system input (in form of definitions, theorems,
algorithms, etc.), system output (mainly in form
of mathematical proofs) and user interaction. When using the Theorema
system, a user should not have to follow a certain style of mathematics
enforced by the system (e.g. basing all of mathematics on set theory or
certain variants of type theory), rather should the system support the
user in her preferred flavor of doing math. The new implementation of
the system, which we refer to as Theorema 2.0, is open-source and
available through GitHub.},
series = {IEEE Explore},
pages = {1--3},
isbn_issn = {ISBN 978-1-5386-2626-9},
year = {2017},
editor = {Tudor Jebelean and Daniela Zaharie},
refereed = {yes},
length = {3},
conferencename = {SYNASC 2017},
url = {http://dx.doi.org/10.1109/SYNASC.2017.00016}
}