Johannes Kepler Symposium on Mathematics

As part of the Johannes Kepler symposium on mathematics Dr. Wolfgang Windsteiger, Research Institute for Symbolic Computation, JKU Linz, will give a public talk (followed by a discussion) on Wed, June 18, 2014 at 15:15 o'clock at HS 13 on the topic of "Mathematical Assistant Systems for Theory Exploration and Mathematics Education" . The organziers of the symposium,

O.Univ.-Prof. Dr. Ulrich Langer,
Univ.-Prof. Dr. Gerhard Larcher
A.Univ.-Prof. Dr. Jürgen Maaß, and
die ÖMG (Österreichische Mathematische Gesellschaft),

hereby cordially invite you.

Series B - Mathematical Colloquium:

The intention is to present new mathematical results for an audience interested in general mathematics.

Mathematical Assistant Systems for Theory Exploration and Mathematics Education

The use of computers to solve mathematical problems has become standard in many domains of mathematics. The systems or programs typically employed are specialized systems providing certain algorithms applicable in the domain of interest, be it (linear) algebra, polynomial equations, differential equations, geometry, special functions, statistics, simulation, or whatsoever. Mathematical assistant systems, on the other hand, are general purpose systems that should be able to support the mathematician during all phases of mathematical activities, regardless of the special domain in which she is working, they are the "pencil and paper of the 21st century'".

Automated and interactive theorem proving are traditionally in the focus of mathematical assistant systems, but also mathematical syntax and notation, organization and reuse of knowledge, the integration of proving and computation, or presentation of mathematics are central topics for any mathematical assistant system. One possible application scenario is the use of mathematical assistants in mathematics education, in particular in the teaching of mathematical logic.

In this talk, we want to present latest developments in the Theorema system, a mathematical assistant system invented and implemented at the RISC institute at JKU.