\documentstyle[11pt]{article}
\begin{document}
\title{General Discussion: {\em Where do we go from here?}}
\author{Deepak Kapur\thanks{e-mail: \tt kapur@cs.albany.edu}}
\date{}
\maketitle

In this last session of the workshop, the following topics were
raised for discussions by the participants.

\begin{enumerate}

\item Do we need a common meta logic? If so, what should it be?

\item How can we build a data base of machine-checked proofs
based on past accomplishments?

\item How can we monitor the progress of different theorem proving
projects vis a vis QED?

\item How should the QED mailing list be administered?

\item When and where should the next meeting be? What form should it take?

\end{enumerate}


{\bf Note:} We briefly elaborate on these topics. Other
participants are requested and encouraged to inform me about the
salient points that I might have missed.

Randall Holmes announced that he had some ideas about a common
meta logic for different theorem provers and proof checkers. He
was planning to write a position paper based on those ideas for
sharing with others. That paper would be available on Holmes' web
page.

Paul Jackson volunteered to maintain a data base of
machine-checked proofs.  He requested other participants to send
him pointers to such data bases being maintained by their
respective groups. Jackson would inform the QED mailing lists
about the site of such a data base and how it could be accessed,
and later, the contents of this data base.

Considerable interest was expressed in learning about the
continued progress being made by different theorem proving and
proof checking systems.  It was suggested that new developments
and progress should be shared with the community by posting them
on the QED mailing list.

A concern was raised that the QED mailing list experiences
occasional bursts of mail messages. Traffic volume increases
considerably, almost to the extent that it becomes difficult for
many of us to keep track of the discussion. The mailing list is
inactive during most of the time though. How does one maintain a
steady flow of contributions to the mailing list?  A moderated
list was proposed as an alternative, but little need was felt for
this change. It was proposed that participants post news items of
interest on the mailing list on a regular basis. Kapur
volunteered to post the abstracts of the papers appearing in {\it
J. of Automated Reasoning} soon when a new issue comes out.
Roman Matuszewski promised to do the same for the Mizar {\it J. of
Formalized Mathematics.} Developers and users of theorem provers
and proof checkers were encouraged to post articles on new
developments and progress related to QED activities made by their
groups.

There was unanimity that both the workshops had been very helpful
in bringing researchers together and highlighting most issues
related to the QED project.  The first workshop was mostly to
familiarize with each other's background, work and interests, and
how they perceived QED and their work in relation to QED. This
was reflected in discussions as well as the round table
organization. The second workshop has been oriented towards a
more structured presentation of topics of interest and relevance
to QED followed by discussions. There was a view that the next
workshop should be in the form of extended abstracts/papers
directly contributing to QED, and a proceedings instead of a
report could be produced at the end of the workshop. Most
participants felt that would be premature, and that it is good to
continue with the format of the second workshop with some minor
changes.

Piotr Rudnicki agreed to look into the possibility of organizing
a workshop at Banff, Canada, sometime in mid May, 1996. No need
was felt to change the way the next workshop should be organized.

\end{document}