## Abstract

On July 20 - 22, 1995, Warsaw University (Bialystok Branch) hosted
the QED Workshop II. The workshop was under the auspices of the State
Committee for Scientific Research (Poland), supported by special funding
from the Office of Naval Research (USA), cosponsored by Microsoft
(Poland) and the Mizar Users Group.

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 814, pp. 238-251, 1994,
and available by anonymous ftp at info.mcs.anl.gov, file pub/qed/manifesto.
The results of the QED Workshop I (1994) are documented in URL
http://www.mcs.anl.gov/qed/.

The workshop was split into one-hour discussions dedicated to specific
problems. Each such discussion was preceded by a short introductory
lecture. Reports of the presentations and discussions are attached below.

## Contents

1. __Introduction__
- Roman Matuszewski -
__(.ps)__
2. __Can we resolve the tension between
constructive type theorists and classical mathematicians?__
- Paul Jackson -
__(.ps)__
3. __The organization of a data base of mathematical knowledge__
- Martin Strecker -
__(.ps)__
4. __Indefiniteness__
- Randall Holmes -
__(.ps)__
5. __Possible use of already formalized mathematical knowledge__
- Manfred Kerber -
__(.ps)__
6. __Reflection: practical necessity or not?__
- John Harrison -
__(.ps)__
7. __Development of analysis in the QED Project__
- Javier Thayer -
__(.ps)__
8. __Mathematical synthesis__
- Peter White -
__(.ps)__
9. __The mutilated checkerboard in set theory__
- John McCarthy -
__(.ps)__
10. __To type or not to type__
- Piotr Rudnicki -
__(.ps)__
11. __Cooperation of automated and interactive theorem provers__
- Ingo Dahn -
__(.ps)__
12. __What are the connections, inter-relations and antipathies
between proof checking and automated theorem proving?__
- Deepak Kapur -
__(.ps)__
13. __ The mutilated chessboard problem __* - checked by Mizar*
- Grzegorz Bancerek -
__(.ps)__
14. __What can QED offer to mathematics?__
- Manfred Kerber -
__(.ps)__
15. __General discussion: __*Where do we go from here?*
- Deepak Kapur -
__(.ps)__

(* romat-16.10.1995*)