The SFB program expired on September 30, 2008. For the link to the successor project click DK Computational Mathematics
Home
Appointments
Papers
Misc
Contact

General Information

News

Projects

-  F1301

-  F1302

-  F1303

-  F1304

-  F1305

-  F1306

-  F1308

-  F1309

-  F1315

-  F1322

People

Abstract


The Theorema project aims at extending current computer algebra systems by facilities for supporting mathematical proving. The present early-prototype version of the Theorema software system is implemented in Mathematica 4.0. The system consists of a general higher-order predicate logic prover and a collection of special provers that call each other depending on the particular proof situations. The individual provers imitate the proof style of human mathematicians and produce human-readable proofs in natural language presented in nested cells. The special provers are intimately connected with the functors that build up the various mathematical domains.

The long-term goal of the project is to produce a complete system which supports the mathematician in creating interactive textbooks, i.e. books containing, besides the ordinary passive text, active text representing algorithms in executable format, as well as proofs which can be studied at various levels of detail, and whose routine parts can be automatically generated. This system will provide a uniform (logic and software) framework in which a working mathematician, without leaving the system, can get computer-support while looping through all phases of the mathematical problem solving cycle:

People

Principal Investigator
Prof. Dr. Tudor Jebelean 9946  mail

Co-Investigators
Prof. Dr. Bruno Buchberger 9941  mail

Scientific Staff
Dr. Martin Giese 9969  mail
DI Laura Kovacs 9939  
DI Nikolaj Popov 9926  
DI Camelia Rosenkranz 9969  

Publications

List of Publications.

Please direct your comments or eventual problem reports to webmaster.

SpezialForschungsBereich SFB F013 | Special Research Program of the FWF - Austrian Science Fund