The Theorema System

Description

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.

Period	20 Feb 2006
Event title	Invited colloquium talk at Carnegie Mellon University, Computer Science seminar
Event type	Other
Location	United StatesShow on map