Gloss of "Inference Engine"

The FDL process builds and applies inference engines according to instructions stored in the FDL and specific to the kind of engine. One extreme would be creating a process "from scratch" on a local machine according to instructions; another extreme would be to simply communicate with an already existing process over the internet. Naturally, different inference engines can be trusted to different degrees not only because of the varying inferences they are intended to check and who programmed them, but also because of the varying reliability of the mechanisms used to run and communicate with them.

Often one tends to think of formal inference steps as "small" and schematic, but inference engines, such as Tactic based engines, can be built that verify arbitrarily complex and non-schematic inferences. A Refiner is an inference engine that generates premises from a conclusion Proposition and a Justification. IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html