(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.
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.