Delivery-Date: 
Message-Id: <199501290923.DAA14504@antares.mcs.anl.gov>
Date: Sun, 29 Jan 95 10:21:17 CET
From: Roman Matuszewski <ROMAT%PLEARN.BITNET@ANLVM.CTD.ANL.GOV>
Subject: QED Workshop Announcement
To: QED Group <qed@mcs.anl.gov>
Sender: owner-qed@mcs.anl.gov
Precedence: bulk


                         QED  WORKSHOP  II
                        July 20 - 22, 1995
                          Warsaw, Poland


HOST: Warsaw University - Bialystok Branch (Mizar Group),

      under the auspices of the State Committee for Scientific
                         Research (Poland),

co-sponsor: Office of Naval Research (USA).

     The goal of this Workshop is to determine whether it is possible
to change the QED Project from a fascinating concept into a practical
cooperation.  QED is the title of an international project to build a
computer system that effectively represents much of important
mathematical knowledge and technique.  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.  A principal application of the QED system will
be the verification of computer programs.  For background on the idea
of the QED Project see "The QED Manifesto" Automated Deduction - CADE
12, Springer Verlag, LNAI, 238-251, 1994, and available by anonymous
ftp at info.mcs.anl.gov:pub/qed/manifesto .  The results of the QED
Workshop I are documented in URL http://www.mcs.anl.gov/qed .


FORMAT OF WORKSHOP:

Our current plan is for the Workshop to be small (30 persons).  We
plan to split the Workshop into one-hour discussions dedicated to
specific problems, such as:

 - how to transform the field under consideration into a branch of
   mathematics or computer science, and what its boundaries would be,

 - identification of the initial mathematical targets,

 - identification of the fields of mathematics to be formalized,

 - why we are needed by mathematics,

 - characterization of the likely use of the QED library by
   mathematicians,

 - consideration of possible use of already formalized mathematical
   knowledge,

 - how to organize the accumulation and reusability of mathematical
   knowledge within QED or in specified systems,

 - how to organize the exchange of information between systems,

 - how to cope with indefiniteness,

 - analysis of the possible use of the QED library in mathematical
   education,

 - database and Internet formats for retrieval,

 - attempt at initiating effective co-operation among projects for QED,

 - discussion of the financing and the co-ordination (where could funding
   be obtained).

Each such discussion will be preceded by an introductory lecture of 20
to 30 minutes.  We will not arrange for a presentation of individual
systems, but it is obvious that when presenting general problems we
will draw experience and examples from the systems which we know best.
We seek speakers for introductory lectures; please feel free to
propose any topic you believe is of general interest.  We are open to
any suggestions.  We will organize also a three-hour panel discussion
at the end of Workshop.

We have financial support for 30 persons, covering the lodging
expenses (hotel and food) and conference fees.  U.S. scientists
interested in financial support for travel to the Workshop should
contact Matt Kaufmann (kaufmann@cli.com).

DEADLINE FOR APPLICATION:  March 31, 1995.  If you are interested
please respond to Roman Matuszewski - Workshop Chairman
(romat@plearn.edu.pl).

Robert Boyer (boyer@cli.com)
Andrzej Trybulec (trybulec@cksr.ac.bialystok.pl)