Glossary FDLnotes

Logical Libraries

Our conception for Formal Digital Libraries involves some functions of ordinary libraries, but is extended to accounting methods for logical relations between documents. Ordinary objects, of varying degrees of structure from informal Text to Formal Proof, are the main content, but the collection also includes documents that serve as certificates of facts established by the processes maintaining the collection. Among the kinds of facts certified by the FDL process are that the ordinary objects it stores were acquired from specific sources or built by specific means (archival functions). These certifications are represented as certificate objects in the FDL. See Certificates.

Our project is especially interested in the certification of formal proofs according to specific (user suppliable) criteria, and when stressing this function, when thinking of the FDL services as principally directed at supporting this function, we call it a "logical library". A particularly esteemed feature a certificate may exhibit is its making an objective and independently verifiable claim; this is the ideal for "logical" claims, and is the alternative to authority. Of course, one might view this as the essence of scientific claims generally, but the procedures for verifying "logical" claims are largely reducible to automatic methods which are in principle directly verifiable by an automated text management process since it can itself in principle perform, and so certify, the computations.

One aspect of ordinary libraries we emulate is theoretical neutrality. Thus, we do not require that ordinary documents must be "correct", indeed there is no privileged criterion for correctness of ordinary texts. Criteria for correctness (via proof engines, eg) are supplied by the users of the FDL as contributions to the text collection.

Certificates in the FDL, however, are guaranteed to be correct according to published criteria; the criteria for certificate correctness must therefore be understandable to users of the "logical library". The correctness of some certificates will be independently verifiable, the ideal for logical claims, but other certificates may not be practically verifiable because they attest to the existence of something that is not made practically accessible (an example being a certificate meaning that there once was a proof of a given formula in the collection).

When a process, say with a user behind it, accesses a collection, the "view" is a sub-collection of objects we call the Current Closed Map served by the FDL and subjected to transformation, perhaps with further copying from the FDL, and is usually stored back to the FDL (see Abstract Ids & Closed Maps). A subtlety is that since Certificates are created only by the FDL process itself, when certificates are to be created in the current closed map, they must be created by the FDL, then added to the current closed map. And since certificates usually refer to objects they are about, those objects must also be in the collection. So one is pretty tightly coupled with an FDL when developing certified content. However, as long as one is only reading from the collection, the coupling can be loose.

This leads us to the matter of Multiple FDLs. Also see FDL Functions for further discussion. IF YOU CAN SEE THIS go to

Glossary FDLnotes