Wolfgang Windsteiger: Theorema: A Mathematical Assistant System based on Mathematica

Abstract: We present the mathematical assistant system “Theorema”, which—as its ultimate goal—tries to provide computer-support for a mathematician during all phases of mathematical activity, such as “defining new concepts from given concepts”, “developing algorithms”, “conjecture properties of concepts/algorithms”, “proving properties of concepts/algorithms”, “publishing results”, etc. Lots of progress has been made in the last 40 years in the development of so-called “computer algebra systems” (e.g. Mathematica, Maple, Axiom, Reduce, Derive, etc.) and automated theorem provers (e.g. TPS, HOL, Vampire, Waldmeister, Isabelle, PVS, etc.) but unfortunately the worlds of “computation” and “proving” have driven apart, at least in the sense of tool-support.

Theorema, designed and directed by Bruno Buchberger at RISC, is an approach to re-unite these separated worlds, i.e. to provide machine-support for both computing AND proving in one uniform frame. In addition to that, the Theorema system tries to support common mathematical textbook-like language in both input and output. The talk will give an overview over the main capabilities of the system and will mostly feature live demos.


Bio: Wolfgang Windsteiger, RISC Linz, Johannes Kepler University Linz, Austria. Studied mathematics in Linz, master's thesis about an implementation of the Groebner bases method supervised by Bruno Buchberger. Member of the Theorema development group at RISC since its foundation approx. 1995. PhD thesis supervised by Bruno Buchberger at RISC about a set theory prover based on Zermelo-Fraenkel set theory in 2001. From January 2006 until April 2006 visting Edmung Clarke at CMU in the frame of the Analytica project.

Maintainer Home > Seminar ]
Last modified: Mon Feb 13 15:28:59 EST 2006