\documentstyle [11pt] {article}
\begin{document}

\title{Introduction}

\author{}\date{}
\maketitle

The QED Workshop II, held in Warsaw on 20--22 July 1995, was the second
meeting devoted to the inchoate QED project.
Robert Boyer and Andrzej Trybulec were responsible for the scientific 
programme, with Roman Matuszewski being the active chair. 

The overall idea of QED is best described by the preamble to the {\em QED
Manifesto} - an anonymously authored document that discusses the 
desirability and feasibility of
organizing a proof-checked encyclopedia of mathematics:

\begin{quote}

  "QED is the very tentative title of a project to build a computer
   system that effectively represents all important mathematical
   knowledge and techniques. The QED system will conform to the
   highest standards of mathematical rigor, including the use of
   strict formality in the internal representation of knowledge
   and the use of mechanical methods to check proofs of the correctness
   of all entries in the system.

   The QED project will be a major scientific undertaking requiring
   the cooperation and effort of hundreds of deep mathematical minds,
   considerable ingenuity by many computer scientists, and broad
   support and leadership from research agencies."

\end{quote}

The first QED Workshop was held at Argonne National Laboratory,
on May 18--20, 1994.  The most important conclusion of that workshop
was that QED was an idea worthy pursuing.  The majority of participants
of the Warsaw workshop subscribed to that conclusion entirely.

The purpose of the workshop was to assemble a group of researchers
to further pursue the idea of building a mechanically proof-checked
encyclopedia of mathematics.  The workshop was run as a sequence of
one hour long discussions each devoted to a specific QED-related topic.
The topics, which were suggested earlier by the participants and accepted
for presentation,  varied from very general issues of
sociological and political nature to specific technical questions.
A short summary of each of the presentations and discussions is attached.

Therefore, the workshop took on the form of a discussion meeting rather
than that of a conventional conference. In the numerous discussions 
a distinction was made between:

\begin{itemize}

\item[(i)] the software that organizes and administers the database of
       mathematical knowledge, and

\item[(ii)] the system or systems that are used to demonstrate the correctness
       of the results in the first place.

\end{itemize}

A clear short term goal was identified: we should attempt making
the results of various systems publicly available, preferably on the
World Wide Web.  Then, over the course of time, we can investigate more
sophisticated ways of integrating the diverse range of the already
accumulated, machine readable mathematical knowledge.

The workshop was attended by 28 researchers, from 9 countries,
representing ongoing worldwide efforts in theorem proving and mathematics.
11 of the participants attended the QED Workshop I at Argonne in 1994.
The list of participants is given below:

\vspace{1ex}{\noindent\bf Australia}

     Rajeev Gore (rpg@cisr.anu.edu.au)

\vspace{1ex}{\noindent\bf Canada}

     Ma{\l}gorzata Korolkiewicz (mkorolki@vega.math.ualberta.ca)

     Bill Pase (bill@ora.on.ca)

     Piotr Rudnicki (piotr@cs.ualberta.ca)

\vspace{1ex}{\noindent\bf Estonia}

     Rein Prank (prank@cs.ut.ee)

\vspace{1ex}{\noindent\bf Germany}

     Bernd Ingo Dahn (dahn@mathematik.hu-berlin.de)

     Wolfgang Jaksch (Wolfgang.Jaksch@informatik.uni-erlangen.de)

     Manfred Kerber (kerber@cs.uni-sb.de)

     Herbert Stoyan (Herbert.Stoyan@informatik.uni-erlangen.de)

     Martin Strecker (strecker@informatik.uni-ulm.de)

     Claus Zinn (Claus.Zinn@informatik.uni-erlangen.de)

\vspace{1ex}{\noindent\bf Japan}

     Yozo Toda (yozo@aohakobe.ipc.chiba-u.ac.jp)

\vspace{1ex}{\noindent\bf Poland}

     Grzegorz Bancerek (bancerek@impan.gov.pl)

     Roman Matuszewski (romat@plearn.edu.pl)

     Bogdan Nowak (bnowak@krysia.uni.lodz.pl)

     Stanis{\l}aw Spie{\.z} (spiez@impan.gov.pl)

     Andrzej Tarlecki (tarlecki@mimuw.edu.pl)

     Andrzej Trybulec (trybulec@cksr.ac.bialystok.pl)

\vspace{1ex}{\noindent\bf Russia}

     Oleg Okhotnikov (okhezinv@math.urgu.e-burg.su)

\vspace{1ex}{\noindent\bf UK}

     John Harrison (John.Harrison@cl.cam.ac.uk)

\vspace{1ex}{\noindent\bf USA}

     Robert Boyer (boyer@cli.com)

     John McCarthy (jmc@sail.stanford.edu)

     William McCune (mccune@mcs.anl.gov)

     Randall Holmes (holmes@math.idbsu.edu)

     Paul Jackson (jackson@cs.cornell.edu)

     Deepak Kapur (kapur@cs.albany.edu)

     Javier Thayer (jt@linus.mitre.org)

     Peter White (peter@opus.geg.mot.com)

\vspace{1ex}

The participants of the workshop shared the opinion that the final shape
of QED will be achieved through a long sequence of small evolutionary steps.
The starting point of this evolution is formed by existing
theorem provers and proof-checkers, especially the ones that have
already accumulated sizable data-bases of machine checked mathematics.

We would like to mention an initiative of John McCarthy who presented a talk
on "Heavy Duty Set Theory" in which he gave examples of inferences
which he felt should be regarded as (mathematically) "obvious" to a practical
proof checker.  He challenged the participants to replicate his solution
of the mutilated checkerboard\footnote{In this Report see: {\em The Mutilated 
Checkerboard in Set Theory}.} 
in various systems and then compare how far the
solutions are from his expectations. As far as I know two systems met the 
challenge. One of these is published in this Report\footnote{{\em The 
Mutilated Chessboard Problem} by Grzegorz Bancerek.}.
For another mutilated checkerboard mechanical checking please see 
{\tt ftp://ftp.cli.com/pub/nqthm/nqthm-1992/examples/subramanian/
\break mutilated-checkerboard.ps} .

There were two general discussions.  The first, a panel discussion
led by Piotr Rudnicki, considered general aspects, as seen
by the 8 panelists (G. Bancerek, M. Korolkiewicz, B. McCune, B. Pase, R. Prank,
S. Spie{\.z}, H. Stoyan, and A. Tarlecki).  The panelists expressed both their
enthusiasm about specialized QED subsystems and reservations about being
too optimistic too soon.  In particular,  there was some discussion
about how to attract mathematicians to the initial steps of building QED.
There were no doubts that when QED is sufficiently developed, mathematicians
will be glad to use it.

The second general discussion, led by Deepak Kapur, concerned
general views on the future of the QED Project (the next workshop,
the need of common meta logic, short term goals, what should be the
administrative structure managing the QED data base, and how to achieve
a steady flow of contributions to the QED mailing list).  The participants
expressed their hope that the next QED Workshop will happen in 1996.

\vspace{3ex}
\rightline{Roman Matuszewski\footnote{Warsaw University, Bia{\l}ystok
Branch, Department of Logic, Liniarskiego street 4, %\hspace{5em}\break
15-420 Bia{\l}ystok, Poland, \tt romat@plearn.edu.pl}}

\rightline{Workshop Chairman}


\end{document}