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