=ADD=
=reftype=
14
=number=
00-19
=url=
ftp://ftp.risc.uni-linz.ac.at/pub/techreports/2000/00-19.zip
=year=
2000
=month=
05
=author=
Vasaru Dupre; Daniela
=title=
Automated Theorem Proving by Integrating Proving, Solving and Computing
=abstract=
The work described in this thesis was developed within the Theorema system.
The aim of Theorema is to provide computer-assisted support to the entire
mathematical exploration cycle in the frame of one uniform logic and one
coherent software system.
To fulfill these requirements one has to combine the power of the computer
algebra systems, widely used in the mathematical community, with the
power of theorem proving systems.
This thesis contributes one step further towards the integration of the
three main activities of mathematical exploration - proving, solving and
computing - into one system.
The main class of provers we designed and implemented, starting from some
ideas of Buchberger, are integrating these three activities.
They are specially designed for properties (in particular, rewrite-properties)
of notions involving alternating quantifiers.
These notions arise, for example, in mathematical analysis: limit, continuity,
differentiability, etc.
Examples of rewrite properties are: "limit of sum is sum of limits",
"the product of continuous functions is continuous", etc.
The automatic generation of this type of proofs is still a challenge for,
if not even beyond the capabilities of current automatic theorem provers.
Using our provers we succeeded in proving automatically the LIM+ challenge
problem together with other similar problems which are beyond the capabilities
of most of the current automatic theorem provers.
Other classes of problems for which we designed and implemented provers
involved definitions by cases, or general formulae over natural numbers or
tuples.
=keywords=
automated theorem proving, integration of automated deduction and computer algebra, computer assisted mathematics, Epsilon-Delta proofs; LIM+ challenge problem
=sponsor=
FWF, project 1302