Author:

• Wolfgang Windsteiger
  RISC Institute, Johannes Kepler University Linz, Austria

Abstract:

The Theorema system is a proof assistant based on Mathematica, one of the leading systems (not only) symbolic computation.
The main aim of Theorema is “natural style”, both in input and in output. From Mathematicawe mainly use its highly programmable notebook interface and the pattern-based programming language. In contrast to other provers in and around the Wolfram/Mathematica-ecosystem, Theorema’s logical engine guiding the proofs does not use any of Mathematica’s builtin algorithms for manipulating symbolic expressions, but has its own language for predicate logic and a proof calculus similar to natural deduction in order to automatically generate human-like proofs. In this tutorial, we want to focus on conditional rewriting and explain its implementation and its applications in the frame of Theorema 2.0. The tutorial will mainly be based on a live demo of the system showing concrete examples of proofs as they are used in teaching logic with the help of Theorema.

Short Bio:

Wolfgang Windsteiger studied Mathematics at the Johannes Kepler University Linz (Austria) and received his PhD from RISC under the supervision of Bruno Buchberger for the development of a set theory prover in the frame of the Theorema system. He earned habilitation in symbolic computation from the Johannes Kepler University Linz (Austria).
His main research interest lies in the development of the Theorema system, in particular in its application in higher education in mathematics and logic.