What happened in the PRL Seminar on FDLs of Nov 17, 2003.

(notes by Stuart Allen)

I led a seminar about aspects of the FDL project pertaining to mechanisms for Mathematical Knowledge Management. There was significant conversation within the seminar.
The seminar agenda was not completed because seminar time was reallocated for more elaboration on Certificate Systems (see below).
Continuation was scheduled for 2 weeks later.

A few of the pages here were prepared specifically for the seminar and were shown, although I have corrected a few minor errors and added some annotations, some filling their own pages.
The label elaboration indicates my attempt to represent further points made in the seminar, by speech or diagram, although my memory may be somewhat mistaken as might be my impressions about the success in seminar of the making various points.
The label remark indicates an attempt to make a point or clarification that was probably not presented in seminar; this seminar report simply provides a natural context for making them, or a chance for some remediation.

Some Tenets about math library design were presented to frame the whole discussion and to address some common misconceptions about our project.

FDL is short for Formal Digital Library.

The first two of the four advertised topics were discussed, namely (1) abstracting from logics and the need for archival methods and (2) a technical conception of certificate system as a basis for accounting for knowledge.

1. Two points emphasized in the first part were that:

   • When you abstract enough from diverse logics, you cease to distinguish formal from informal inference, since one possible program for verifying a purported inference may be to ask an individual for confirmation, and record that confirmation as a fact.
     Such a program is the formal face of an informal process of validation.
     This observation may emphasize both the importance of accounting for how claims to knowledge are established in a library, and the potential for embracing informal methods within a formal accounting system.
   • Applied logicians and archivists have tended to develop complementary aspects of articulating knowledge, the former concentrating on the internal linguistic formal features of correct inference, the latter on the external features relating records of fact (as well as other texts referenced by records) that support claims to knowledge. (elaboration)

2. The audience was especially interested (as am I) in Certificate Systems, so much of the seminar period was spent discussing them instead of moving on to the the last two topics. A Simplified Certificate System was described to give the basic idea of how to flexibly constrain a generic system of computationally verified claims in a way that makes it possible to make significant inferences from the mere existence of a given library object.

   In response to audience discussion, diagrams were drawn providing details on certificate structure and illustrating the relations between certificates and objects supposed to represent inferences (elaboration). Also described were how one might design kinds of certificates to verify inference steps by calls to external processes (external to the library process that is), and how one might design kinds of certificates to assemble verified proofs from collections of verified or purported inference steps.

   Audience demand also initiated discussion of Certificate Systems in which certificates can be reconsidered for update when texts they depend on have been altered. Discussion continued 2 weeks later.