Gloss of "Tactic"

Some Inference Engines are tactic based provers. They are significant as examples of systems that can accept wide variety of complex Inference Steps, and that can be rather expensive to run due to the fact that tactics may be programs built in a full general purpose programming language.

When such an inference engine is built, one typically builds a state with a lot of procedures and data built in.

In the following explanation of what tactics are, the notion of proof is internal to the tactic prover, and is not presumed to be that of Proof as used in the FDL. The principal use of the tactic prover by the FDL process is simply as a source of individual inferences.

Given a collection of prespecified "primitive" inference forms, a tactic is a program for reducing a desired proof goal to premises by composing primitive inferences. A tactic is essentially a program for constructing such an inference tree, and one chooses which tactics to apply according to how you want to generate subgoals from the goal. The execution of the tactic gives rise to an inference step, the premises being all the unproved leaf premises of the primitive proof tree. Further, to count as a tactic, although its execution might not terminate or might raise an exception, if it does terminate without exception, then it must be guaranteed to generate subgoals justifiable by primitive inferences.

Returning to the concept of FDL Proof, an alternative use of a tactic prover by the FDL would be to call the tactic prover's bluff and demand that the tactic prover produce for the FDL the smaller inferences that it claims existed. A tactic prover providing this alternative access by the FDL process could then be double checked in order to provide an independent verification of the original complex inference.

The appropriate form of Justification used in an Inference Step to be submitted to a tactic prover is the tactic code for it to execute. An inference engine that generates its premises from conclusion and justification, as in the process described above, is called a Refiner. IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html