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.
Forschungs-