=ADD=
=reftype=
14
=number=
98-25
=url=
ftp://ftp.risc.uni-linz.ac.at/pub/techreports/1998/98-25.ps.gz
=year=
1998
=month=
12
=author=
Buchberger; Bruno + Aigner; Klaus + Dupre; Claudio + Jebelean; Tudor + Kriftner; Franz + Marin; Mircea + Nakagawa; Koji + Podisor; Ovidiu + Tomuta; Elena + Usenko; Yaroslav + Vasaru; Daniela + Windsteiger; Wolfgang
=title=
{\em Theorema}: An Integrated System for Computation and Deduction in Natural Style
=abstract=
The {\em Theorema} project aims at integrating computation and deduction in a
system that can be used by the working scientist for building and checking
mathematical models, including the design and verification of new algorithms.
Currently, the system uses the rewrite engine of the computer algebra system
{\em Mathematica} for building and combining a number of automatic/interactive
provers (high-order predicate-logic, induction for lists/tuples and natural
numbers, etc.) in natural deduction style and in natural language presentation.
These provers can be used for defining and proving properties of
mathematical models and algorithms, while a specially provided ``computing
engine'' can execute directly the logical description of these algorithms.
=howpublished=
CADE 98 (Computer Aided Deduction), Lindau, Germany, July 1998, Workshop on Integrating Computation and Deduction
=sponsor=
Austrian Science Foundation (FWF), project FO-1302 (SFB).
=keywords=
automated reasoning