Message-Id: <199512031454.QAA27130@ra.abo.fi>
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
Date:         Sun, 03 Dec 95 15:13:11 CET
From: Roman Matuszewski <ROMAT%PLEARN.BITNET@PLEARN.EDU.PL>
Subject:      QED II - final report - available
To: qed@mcs.anl.gov
Cc: wachter@itd.nrl.navy.mil, D.Scott@newton.cam.ac.uk,
        bra-types@cs.chalmers.workserver.ai.mit.edu,
        info-hol@leopard.cs.byu.edu, lics@research.att.com,
        theorem-provers@mc.lcs.mit.edu


I  inform  the  QED  community,  that

    the final report of the QED Workshop II (1995)
    ----------------------------------------------

held  in  Warsaw,  is  located  on  the  "QED home page":

    http://www.mcs.anl.gov/qed/index.html
    -------------------------------------

at Argonne National Laboratory (thanks to Bill McCune, who installed
there my html files).

The report is prepared in LaTeX and PostScript version (also gziped).

Besides the QED II final report, you can also find there the results of
the QED Workshop I (1994), the archive of the qed mailing list, the QED
Manifesto and related links.

===========================================

Because the QED Workshop II was a few months ago, I would like to remind
some information:

The workshop was attended by 28 researchers from 9 countries.
In the final report we publish (besides my Introduction) following
articles:

- Can we resolve the tension between constructive type theorists
  and classical mathematicians  - by Paul Jackson

- The organization of a data base of  mathematical knowledge  -
  by Martin Strecker

- Indefiniteness - by Randall Holmes

- Possible use of already formalized mathematical knowledge -
  by Manfred Kerber

- Reflection; Practical necessity or not - by John Harrison

- Development of analysis in the QED Project - by Javier Thayer

- Mathematical synthesis - by Peter White

- The mutilated checkerboard in set theory - by John McCarthy

- To type or not to type - by Piotr Rudnicki

- Cooperation of automated and interactive theorem provers - by Ingo Dahn

- What are the connections, inter-relations and antipathies between proof
  checking and automated theorem proving - by Deepak Kapur

- The mutilated chessboard problem (checked by Mizar) -
  by Grzegorz Bancerek

- What can QED offer to mathematics - by Manfred Kerber

- General discussion: where do we go from here - by Deepak Kapur

I would like to mention an initiative of John McCarthy who presented a
talk on "Heavy Duty Set Theory" (in the report published as "The mutilated
checkerboard in 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
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 ("The Mutilated Chessboard Problem" by G.Bance-
rek). For another mutilated checkerboard mechanical checking please see
ftp://ftp.cli.com/pub/nqthm/nqthm-1992/examples/subramanian
    /mutilated-checkerboard.ps .

Robert Boyer (CLInc.) and Andrzej Trybulec (Warsaw University) were respon-
sible for the scientific programme, with me as the workshop chairman.

The workshop was under the auspices of the State Committee for Scientific
Research (Poland), supported by the Office of Naval Research (USA), cospon-
sored by Microsoft (Poland) and the Mizar Users Group.

===========================================

In the hope of provoking discussion on our m-list I would like to ask:
 - are there any other examples of solution of problem given by John
   McCarthy,
 - what do you think about questions given above by the authors in
   the report.

I see the presentation of solution of the mutilated checkerboard in
various systems and then as comparison of them, as really important
exchange of the practical experience which we need in the QED Project.


-- Roman Matuszewski