\documentstyle[11pt]{article}
\begin{document}
\title{The organization of a data base of mathematical knowledge}
\author{Martin Strecker\thanks{e-mail: \tt strecker@informatik.uni-ulm.de}
\\ University of Ulm, Germany}
\date{}
\maketitle

The talk started with a survey of the main difficulties the QED project has to
face. These are, among others:
\begin{itemize}
\item Different foundational formalisms
\item Different concepts of validity of theorems
\item Consequently, different calculi yielding different proofs
\end{itemize}
Two different approaches can be envisaged for solving these difficulties. On
the one hand, one can define a ``root logic'' serving as a meta-language for
expressing and communicating statements and proofs developed in the particular
object logics. Such an approach was judged to be a rather far-reaching goal
not attainable in the near future.

On the other hand, a database of formalized mathematics and computer science
can be constructed, starting from the large corpus of theories developed for
some of the current systems. Apart from demonstrating the utility and
applicability of formalized mathematics to ``the public'', such a database
could improve the exchange of results within the QED community. For meeting
this goal, the database would have to include a detailed description of objects,
 such as:
\begin{itemize}
\item Terminology, definitions
\item Axiomatizations
\item Mathematical theories
\item Theorems
\item Proofs and proof methods / tactics
\end{itemize}
A theory could for example be indexed by the following information:
\begin{itemize}
\item On which other theories does it depend?
\item  Which theories does it extend?
\item Are there theory interpretations to other theories?
\item Over which theories is it parameterized?
\end{itemize}

Apart from that, some meta-information would have to be added in order to
account for different philosophies of mathematics. Such information might
detail whether a proof uses a constructive or non-constructive argument
or whether it is based on a contested axiom.


The discussion following the talk centered on the problem of retrieving
information from a database. Since most information is currently stored in the
form of text files, it is difficult to organize the data in such a way that
they are amenable to ``semantic'' queries as opposed to a purely textual
search. In particular, experience shows that finding previously proved
theorems is a serious problem. It seems that so far no adequate solutions for
these problems are known and further research on this topic is necessary.

Another issue addressed during this discussion (and resumed in several other
occasions) was the question of whether QED should get involved in foundational
debates, for example when deciding on the structure and contents of a database,
or whether QED had not better develop practical methods for making existing
formalizations accessible and for combining them. This could
eventually lead to a methodology of problem solving similar to the approach
advocated in software engineering: Decomposing a given problem into
subproblems, until solutions can be found by the aid of powerful libraries.


One of the tangible results of the discussion was the proposal to provide easy
access to the systems developed in the QED context via WWW. Links
to systems could be kept on a centralized WWW page. By activating a link, the
 user
could start a session with the respective system and either initiate proof
tasks or at least submit queries about certain theories. It was mentioned that
some systems (Nuprl, IMPS) already provide some of these services or will soon
 make them
available.
\end{document}