Johannes Kepler Symposium für Mathematik
Im Rahmen des Johannes-Kepler-Symposiums für Mathematik wird Dr. Wolfgang Windsteiger, Research Institute for Symbolic Computation, JKU Linz, am Wed, June 18, 2014 um 17:15 Uhr im HS 13 einen öffentlichen Vortrag (mit anschließender Diskussion) zum Thema "Mathematical Assistant Systems for Theory Exploration and Mathematics Education" halten, zu dem die Veranstalter des Symposiums,O.Univ.-Prof. Dr. Ulrich Langer,
Univ.-Prof. Dr. Gerhard Larcher
A.Univ.-Prof. Dr. Jürgen Maaß, und
die ÖMG (Österreichische Mathematische Gesellschaft)
hiermit herzlich einladen.
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.