=ADD=
=reftype=
14
=number=
99-46
=url=
ftp://ftp.risc.uni-linz.ac.at/pub/techreports/1999/99-46.tar.gz
=year=
1999
=month=
07
=author=
Buchberger; Bruno
=title=
Theory Exploration Versus Theorem Proving
=abstract=
Computer-aided Theorem Proving is often considered to be the problem of
generating a proof for (or, at least, deciding about the truth of) a given
goal proposition under given assumptions. The power of automated or
interactive theorem provers is then measured by the class of propositions
and assumptions for which proofs can be generated. In this talk, we want to
introduce and study a different paradigm, {\em Computer-Aided Theory
Exploration}, which models the actual research and teaching situation of
mathematicians in a more natural way. We will show, by examples from
various parts of mathematics, how an {\em exploration situation} is
characterized by the following parameters: "known notions", "known facts
about known notions", a "new notion", "axioms that relate the new notion
with the known notions", and finally, "a class of goal propositions that
completely explore the relation of the new notion with the known notions".
We will argue that these parameters suggest the construction of a special
(automated or semi-automated) prover that is "appropriate" for the given
exploration situation. In the construction of the appropriate prover, it
seems to be crucial that some of the facts about the known notions are
transformed from their status as being just propositions into the status of
establishing special inference rules (or, more generally, proof
techniques). This transformation seems to be crucial for arriving at the
automated generation of "short" proofs that imitate the natural proof style
of mathematicians. Our study will be given in the frame of the
{\em Theorema}
software system, which is currently being developed by the {\em Theorema}
Working Group at RISC under the direction of the author
(www.theorema.org).
=howpublished=
Invited talk at Calculemus 99, Trento, Italy, July 1999
=sponsor=
SFB/FWF project F1302
=keywords=
automatic reasoning