Information Technology Reference

In-Depth Information

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/
.

Search WWH ::

Custom Search