We are building a Formal Digital Library (FDL) of algorithmic
mathematics.
In advance of developing the FDL itself to the point where a community
of clients can directly access and contribute to it, we present examples of
texts in the form of web pages in order to show the nature of formally
grounded texts. The inter-connectivity between texts exposing logical
dependencies is of particular note.
Full access to the FDL will be effected by Application Program Interfaces
to collections of diverse formal material, such as proofs and algorithms,
as well as informal explanations grounded in such material. One aspect of
this diversity will be differences in the formal systems in which
the formal texts are couched, and the FDL design is open to client
specified criteria of form and correctness.
|
|
