Gloss of "Inference Step"

By this we mean the kind of data typically intended to express a logical inference from zero or more premises to a conclusion. An Inference Engine is the device that is employed by the FDL process to generate or check an inference step.

An inference step is represented as an individual Object (rather than being simply a subexpression of a Proof) because the cost of individual inference steps can be expected to dominate the cost of checking a proof. The organization of inference steps into proofs is rather cheap, and there is benefit to making inferences checkable independently of the proofs they occur in.

An FDL process checks or generates an inference step by applying an Inference Engine, which is usually a process whose creation is according to user specified methods. The inference step comprises expressions for each Proposition of the conclusion or premises, as well as a Justification which may be used by inference engines to restrict what counts as an inference of that type. The same inference can be verified by any number of different inference engines since the fact that a given inference has been verified by a given engine is expressed as the content of a Certificate which is external to the inference and refers to it. IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html