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

Of course, the way it is sketched above, things cannot work: We are mixing
language levels here. For example, the ' ' in the previous formula occurs twice

but on different language layers and we must not use the same symbol for these
two occurrences. Similarly, the '

∀

∀ ' in the definition of tuple-induction has to be

different from the ' ' in the definition of sort . In fact, in the above sketch of an

exploration session, we are migrating through three different language layers.
We could now use separate name spaces for the various language layers. How-
ever, this may become awkward. Alternatively, one has to introduce a “quoting
mechanism”. The problem has been, of course, addressed in logic, see [22] for
a recent discussion but we think that still a lot has to be done to make the
mechanism practical and attractive for the intended users of future reasoning
systems. In Theorema, at present, we are able to define algorithms and formu-
late theorems, apply algorithms and theorems to concrete inputs (“compute”)
and prove the correctness of algorithms and theorems in the same session and
using the same language, namely the Theorema version of predicate logic. For
this, the name spaces are automatically kept separate without any action needed
from the side of the user. However, we are not yet at the stage where we could
also formulate provers and prove their correctness within the same language and
within the same session. This is a major design and implementation goal for the
next version of Theorema. An attractive solution may be possible along the
lines of [25] and [26].

∀

8Con lu on

We described mathematical theory exploration as a process that proceeds in a
spiral. In each cycle of the spiral, new axioms (in particular definitions), propo-
sitions, problems, and methods (in particular algorithms) are introduced and
studied. Both invention of axioms, propositions, problems, and methods as well
as verification of proposition and methods can be supported by algorithms (“al-
gorithmic reasoners”). For this, at any stage of an exploration, we have to be able
to act both on the object level of the formulae (axioms, propositions, problems,
methods) and the meta-level of reasoners. We sketched a few requirements future
mathematical exploration systems should fulfil in order to become attractive as
routine tools for the exploration activity of working mathematicians.
A particular emphasis was put on the interaction between the use of schemes
(axiom schemes, proposition schemes, problem schemes, and algorithm schemes)
and the algorithmic generation of conjectures from failing proofs as a general
heuristic, computer-supportable strategy for mathematical invention. The po-
tential of this strategy was illustrated by the automated synthesis of the author's
Grobner bases algorithm. The ideas presented in this paper will serve as work
plan for the next steps in the development of the Theorema system.

References

1. An Interactive Mathematical Proof System. http://imps.mcmaster.ca/ .
2. The Coq Proof Assistant. http://coq.inria.fr/ .
3. The Mizar Project. http://www.mizar.org/ .