Algorithm-Supported Mathematical Theory Exploration: A Personal View and Strategy - Artificial Intelligence and Symbolic Computation - page 236

Algorithm-Supported
Mathematical Theory Exploration:
A Personal View and Strategy

Bruno Buchberger

Research Institute for Symbolic Computation
Johannes Kepler University Linz
A-4040 Linz, Austria
[e-mail]

Abstract. We present a personal view and strategy for algorithm-sup-
ported mathematical theory exploration and draw some conclusions for
the desirable functionality of future mathematical software systems. The
main points of emphasis are: The use of schemes for bottom-up math-
ematical invention, the algorithmic generation of conjectures from fail-
ing proofs for top-down mathematical invention, and the possibility to
program new reasoners within the logic on which the reasoners work
(“meta-programming”).

1 A View of Algorithm-Supported

Mathematical Theory Exploration

Mathematical theories are collections of formulae in some formal logic language
(e.g. predicate logic). Mathematical theory exploration proceeds by applying,
under the guidance of a human user, various algorithmic reasoners for producing
new formulae from given ones and aims at building up (large) mathematical
knowledge bases in an ecient, reliable, well-structured, re-usable, and flexible
way. Algorithm-supported mathematical theory exploration may also be seen as
the logical kernel of the recent field of “Mathematical Knowledge Management”
(MKM), see [10] and [5]. In the past few decades, an impressive variety of results
has been obtained in the area of algorithm-supported reasoning both in terms of
logical and mathematical power as wells as in terms of software systems, see for
example, ALF [18], Automath [12], Coq [2], Elf [21], HOL [13], IMPS [1],

Sponsored by FWF ( Osterreichischer Fonds zur Forderung der Wissenschaftlichen
Forschung; Austrian Science Foundation), Project SFB 1302 (“Theorema”) of the
SFB 13 (“Scientific Computing”), and by RICAM (Radon Institute for Computa-
tional and Applied Mathematics, Austrian Academy of Science, Linz). The final
version of this paper was written while the author was a visiting professor at Kyoto
University, Graduate School of Informatics (Professor Masahiko Sato). I would like
to thank my coworkers A. Craciun, L. Kovacs, Dr. T. Kutsia, and F. Piroi for dis-
cussions on the contents of this paper, literature work, and help in the preparation
of this paper.