Notes by sfa about the Formal Digital Library (see FDL project page).

These are working notes explaining the purposes and design of Formal Digital Libraries.

The article Abstract Identifiers, Intertextual Reference and a Computational Basis for Recordkeeping, based on these notes, elaborates on our basic concepts and methods for managing inter-referential digitally stored texts with the special aim of accounting for logical dependencies upon which meaningfulness and correctness of these "formal" texts depends. We are also especially concerned with safe sharing of formal texts among diverse clients who may not fully agree on what constitutes meaningful and correct material.

These working notes are considerably more detailed than the paper mentioned above, and cover concepts not discussed in the paper.

There is a Glossary.

1.	Content vs Infrastructure	550 wds
2.	Formal vs Informal	270 wds
3.	Words vs Formality	410 wds
4.	Bates's Point	130 wds
5.	Readings	440 wds
6.	Concise Informal Annotations	620 wds
7.	Logical Libraries	490 wds
8.	Multiple FDLs	560 wds
9.	FDL Functions	640 wds
10.	Abstract Ids & Closed Maps	490 wds
11.	Closed Maps	300 wds
12.	Closed Map Operations	220 wds
13.	Closed Map Operations (merge)	310 wds
14.	Closed Map Operations (split,clone,fold)	300 wds
15.	Conservation and Destruction	80 wds
16.	Abstract Identifiers (how)	440 wds
17.	Pro-textual Constituents	420 wds
18.	Naming Problems	550 wds
19.	Abstract Id Allocation	450 wds
20.	Adequacy of Single Id Space	380 wds
21.	Certificates	540 wds
22.	Certificate Bias	510 wds
23.	Certificate Significance	590 wds
24.	Conflicts of Significance	570 wds
25.	Certificate Structure	640 wds
26.	Borrowed Certificates	450 wds
27.	Certificate Identifiers	240 wds
28.	Current Closed Maps	400 wds
29.	Initial Closed Map	420 wds
30.	Altering Certificates	510 wds
31.	Stale Certificates	400 wds
32.	Staleness (pertinence)	490 wds
33.	Staleness (extra state)	490 wds
34.	Staleness (deletion)	330 wds
35.	Staleness (resolution)	470 wds
36.	Assimilation to Certificates	180 wds
37.	Processes	640 wds
38.	Proof Organization	470 wds
39.	Proof Certification	360 wds
40.	Lemma Citation	590 wds
41.	Proof Sentinels	670 wds
42.	Proof Sentinels (continued)	400 wds
43.	Sharing Formal Mathematics	130 wds
44.	Forms of Sharing Math	530 wds
45.	What Math can be Shared	590 wds
46.	Scenarios of FDL Use	690 wds
47.	Scenarios of FDL Use(part 2)	480 wds
48.	Scenarios of FDL Use(part 3)	530 wds
49.	Scenarios of FDL Use(part 4)	470 wds

GLOSSES:

1.	Abstract Identifiers	80 wds
2.	Blob	110 wds
3.	Certificate	250 wds
4.	Client	130 wds
5.	Closed Map	90 wds
6.	Current Closed Map	40 wds
7.	Definition	160 wds
8.	External Name	180 wds
9.	FDL	220 wds
10.	Formal	140 wds
11.	Inference Engine	150 wds
12.	Inference Step	210 wds
13.	Justification	170 wds
14.	Name Server	170 wds
15.	Native Language	240 wds
16.	Object	70 wds
17.	Pro-textual Constituents	20 wds
18.	Proof	230 wds
19.	Proposition	370 wds
20.	Refiner	50 wds
21.	Sentinel	70 wds
22.	Session	80 wds
23.	Tactic	350 wds
24.	Term	30 wds
25.	Text	330 wds
26.	Text Server	90 wds

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html