Mission
As
a matter of fact, automated reasoning (automated theorem proving)-
despite impressive advances in the reasoning technology - so far had very
little influence on the every-day
work of mathematicians, whereas it had quite some impact on a few
selected application areas like logic programming, hardware verification,
and artificial intelligence. We believe that the reason for this is that
main stream automated reasoning focused on
–
the automated proof of isolated theorems (given a certain knowledge base,
mostly axioms), see the typical examples in the CADE theorem proving
competition
–
and the usage of general reasoning methods (like the resolution method)
uniformly for all areas of mathematics. In contrast, the practical
reasoning activities of "working mathematicians" proceed
–
by building up theories in structured layers (inventing definitions,
inventing and proving lemmata and theorems, inventing problems, inventing
and proving algorithms) so that in most of the incremental steps
relatively easy proving is sufficient
–
and by using many different special reasoning techniques for the various
theories at hand.
We
believe that this structured and theory-dependent approach to
mathematical reasoning is the reason why, for human mathematicians,
building up complicated mathematical theories is possible at all.
Therefore,
in the talk "Theorem Proving Versus Theory Exploration" at the
Calculemus Workshop in Trento 1999 and in the Workshop "Mathematical
Knowledge Management (MKM)" which we organized, for the first time
2001 at RISC, we advocated that,
at least for the application of automated reasoning in mathematics, we
should shift the attention to the
Automation of Mathematical Theory Exploration rather than considering
only the proof of isolated theorems. In the meantime, quite some
researchers have started to work in the area of Mathematical Knowledge
Management (documented in the series of MKM conferences).
In
this Workshop AUTOMATHEO (Automated Mathematical Theory Exploration) we
gather for discussing approaches to one particularly challenging and not
yet heavily studied aspect of automated theory exploration, namely the
computer-supported invention
of definitions, theorems, problems, and algorithms, which of course
cannot be seen independent of proving. We hope that from this first meeting of
groups working in the area of automated invention in mathematics some
impulse will be generated for more intensive studies in this area in the
future and we will be happy to organize AUTOMATHEO Workshops also in the
future.
Bruno Buchberger
Founder
of the Research Institute for Symbolic Computation
|