| Abstract Identifiers
|
identifiers treated abstractly and as atomic, serving as Object names in a Closed Map
|
|
|
| Blob
|
an atomic value for which equality might not even be implemented
|
|
|
| Certificate
|
an Object attesting to some fact established by the FDL process
|
|
|
| Client
|
an entity, such as a person, supposed normally to exist and perhaps persist outside the FDL process, with which the FDL interacts Sessions and for which it maintains certain privileges
|
|
|
| Closed Map
|
a finite collection of named Objects; the names are Abstract Identifiers, the contents are Texts; objects can refer to objects
|
|
|
| Current Closed Map
|
the main part of the state in a Session with a Client of the FDL, being a distinguished, variable Closed Map
|
|
|
| Definition
|
an explicit eliminable definition of a mathematical operator or concept
|
|
|
| External Name
|
a concrete name whose association to Abstract Identifiers is maintained by the FDL; "external" emphasizes the contrast with abstract identifiers which are "internal" to an FDL
|
|
|
| FDL
|
Formal Digital Library; a repository of a certain kind with a process for using it
|
|
|
| Formal
|
having precise meaning or objective criteria of correctness, ideally computer verifiable, based simply upon "syntactic" form
|
|
|
| Inference Engine
|
a process that can verify (or generate) an Inference Step
|
|
|
| Inference Step
|
expression of an inference from zero or more premises
|
|
|
| Justification
|
data provided to an Inference Engine in an Inference Step in addition to its Propositions
|
|
|
| Name Server
|
an association of "names" with Closed Maps or Objects
|
|
|
| Native Language
|
a programming notation executable by the FDL process
|
|
|
| Object
|
the unit of FDL content; abstractly named Texts
|
|
|
| Pro-textual Constituents
|
the constituents of Texts that are not themselves texts
|
|
|
| Proof
|
a complex of appropriately related Inference Steps
|
|
|
| Proposition
|
an expression used as a conclusion or premise of an Inference Step
|
|
|
| Refiner
|
an Inference Engine that computes premises from a conclusion and Justification
|
|
|
| Sentinel
|
an expression occurring in a Certificate validating an Inference Step identifying which primitive logical resources are permitted in justifying it; the unit of coherency in Proofs
|
|
|
| Session
|
a subprocess of the FDL, with associated state, for communication with a Client
|
|
|
| Tactic
|
a program describing an inference by composing primitive inferences
|
|
|
| Term
|
synonym for Text; the main form used in the FDL for structured data such as expressions
|
|
|
| Text
|
the main form used in the FDL for structured data such as expressions
|
|
|
| Text Server
|
the aspect of an FDL as a process exchanging Texts with Clients
|