Theorema: Theorem Proving for the Masses Using Mathematica

Bruno Buchberger

Download talk material:

Bruno Buchberger

The Theorema project aims at bringing computer-supported mathematical proving into the frame of Mathematica, using both the logical power of Mathematica's rule-based programming style and the flexibility and maturity of Mathematica's front end. Theorema generates proofs in natural languages in the style of proofs produced by humans. Applications range from logical training for students to computer-supported mathematical research and formal software verification.

Bruno Buchberger, Ph.D., is full professor of computer mathematics at the Johannes Kepler University in Linz, Austria. He is the inventor of the Gröbner Bases method for computer algebra. In 1987, he founded RISC (Research Institute for Symbolic Computation), Austria. He is also founding editor of the Journal of Symbolic Computation and founder and director of the Software Park Hagenberg, Austria.