|
Theorema: Theorem Proving for the Masses Using
Mathematica
Bruno Buchberger
RISC-Linz
Download talk material:
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.
|