Delivery-Date: 
Message-Id: <199507281637.LAA13935@antares.mcs.anl.gov>
Date: Fri, 28 Jul 95 18:36:28 CET
From: Roman Matuszewski <ROMAT%PLEARN.BITNET@ANLVM.CTD.ANL.GOV>
Subject: QED Workshop II
To: qed@mcs.anl.gov
cc: bra-types@cs.chalmers.sw, info-hol@leopard.cs.byu.edu, 
    lics@research.att.com, theorem-provers@mc.lcs.mit.edu
Sender: owner-qed@mcs.anl.gov
Precedence: bulk


I would like to inform the QED community about the last
QED Workshop, held in Warsaw, this July, 20 - 22.

The workshop was under the auspices of the State Committee
for Scientific Research (Poland) and co-sponsored by
the Office of Naval Research (USA) and Microsoft (Poland).

The Mizar Group hosted 28 attendees from 8 countries
(the list is given below) in the governmental conference
center in Warsaw. 11 persons participated second time round
in this event. Despite high temperatures, the workshop
covered all planed topics.

John McCarthy presented a talk showing inferences which
he felt should be regarded as (mathematically) "obvious",
and he proposed solving the Mutilated Checkerboard in Set
Theory in various systems.

There were two general meetings. One - panel discussion -
led by Piotr Rudnicki, considered general aspects, as seen
by the 8 panelists (B.Pase, R.Prank, H.Stoyan, G.Bancerek,
St.Spiez, A.Tarlecki, B.McCune, M.Korolkiewicz).
The second general discussion, led by Deepak Kapur, concerned
general views on the future for the QED Project (e.g. future
conference, meta logic, what do we do next, short term goals,
admin. structure, future of the QED mailing list, ...).

Now we are in the time of preparation of the final report, which
will be presented on the QED m-list.

-- Roman Matuszewski

-------------------------------------------------------------

                    QED Workshop II,
               Warsaw, July 20 - 22, 1995

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

CANADA
     Malgorzata Korolkiewicz (mkorolki@vega.math.ualberta.ca)
     Bill Pase (bill@ora.on.ca)
(*)  Piotr Rudnicki (piotr@cs.ualberta.ca) - To type or not to type

ESTONIA
     Rein Prank (prank@cs.ut.ee)

GERMANY
(*)  Bernd Ingo Dahn (dahn@mathematik.hu-berlin.de) - Cooperation
                      of automated and interactive theorem provers,
     Wolfgang Jaksch (Wolfgang.Jaksch@informatik.uni-erlangen.de)
(**) Manfred Kerber (kerber@cs.uni-sb.de) - Possible use of already
                     formalized mathematical knowledge,
                   - Why we are needed by mathematics,
     Herbert Stoyan (Herbert.Stoyan@informatik.uni-erlangen.de)
(*)  Martin Strecker (strecker@informatik.uni-ulm.de) - The organization
                      of a data base of mathematical knowledge,
     Claus Zinn (Claus.Zinn@informatik.uni-erlangen.de)

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

POLAND
(*)  Grzegorz Bancerek (bancerek@impan.gov.pl) - Mizar proof of the
                                          mutilated checkerboard problem,
     Roman Matuszewski (romat@plearn.edu.pl)
     Bogdan Nowak (bnowak@krysia.uni.lodz.pl)
     Stanislaw Spiez (spiez@impan.gov.pl)
     Andrzej Tarlecki (tarlecki@mimuw.edu.pl)
(**) Andrzej Trybulec (trybulec@cksr.ac.bialystok.pl) - Computer
                       reconstruction of mathematical technology,
                     - Syntax vs. semantics,

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

UK
(*)  John Harrison (John.Harrison@cl.cam.ac.uk) - Reflection: practically
                    necessary or not,

US
     Robert Boyer (boyer@cli.com)
(*)  John McCarthy (jmc@sail.stanford.edu) - Heavy duty set theory,
     William McCune (mccune@mcs.anl.gov)
(*)  Randall Holmes (holmes@math.idbsu.edu) - Indeterminateness,
(*)  Paul Jackson (jackson@cs.cornell.edu) - Can we agreeably resolve
                   the tension between type theorists  (constructivists,
                   de Bruijn, Martin Lof, Constable) and  the classical
                   mathematicians?
(*)  Deepak Kapur (kapur@cs.albany.edu) - What are the connections,
                   interrelations, and antipathies between proof
                   checking and automatic theorem proving?
(*)  Javier Thayer (jt@linus.mitre.org) - Formalized Analysis
(*)  Peter White (peter@opus.geg.mot.com) - Mathematical synthesis