Information-Intensive Proof Technology
by Robert L. Constable
Published version from Proof Technology and Computation [PDF]
Article and Lecture Notes for the Marktoberdorf NATO Summer School, 2003.
Introduction to the Notes
We are going to stress the theme that theorem provers can accomplish more if they work together. It seems clear that there will always be several different provers supported at any one time. They will use different logics, incompatible logics, and yet we will want to collect their general results together and attempt to share them and use them in research and applications. How can this be done?
There are groups collecting formal mathematics and presenting it on the Web, e.g., HELM, OMDoc, and our Formal Digital Library. Our project is concerned with the logical issues behind organizing these collections, and with some of the digital library issues, such as collecting formal metadata.
The plan of these lectures is to first explore the logical problems of sharing and show some solutions, referring to the work of Doug Howe, Pavel Naumov, Messeguer, and Stehr, and recent work of Evan Moran. Then we will look at some technical issues of a logical nature in creating a logical library of formalized mathematics.
In the last two lectures I will illustrate how provers with sufficiently large libraries are able to formalize and verify protocols at speeds close to those of the designers and programmers as they create them. This will also be an opportunity to discuss formal elements of our approach to formalizing concepts from distributed computing.
bibTex ref: Con06