Specify Proof Directives

   If the user has asked to specify proof directives on the menu Set SPECWARE Parameters, under the item Customize (), a menu appears entitled Specify Proof Directives for Spec. This menu contains the following items:

Specify induction tactics?

  Select Yes if you wish to use the induction rule on any of the conjectures in the current batch. 

Specify prover usage of Spec axioms/theorems:

   This item controls how the axioms of the axiom list are to be used in proving the conjecture. Several options are offered. At this stage, the user is expected to select all those that might be wanted for some axiom. In other words, if in doubt, select all of them. The selected options will then be offered for each axiom on the axiom list.

The options offered are as follows; in each case, we say what will happen if the option is selected. More than one may be chosen:

Rewrite

The axiom will be used as a rewrite (simplification) rule (see ). Only equalities may be rewrite rules.    

Forward

The axiom may be used in the forward inference phase (see ).

Backward

The axiom may be used in the backward inference phase (see ) .

left-to-right

The axiom (an equality) may be used to replace instances of its left side by corresponding instances of its right side 

right-to-left

The axiom may be used to replace instances of its right side by corresponding instances of its left side. An axiom may be used both left to right and right to left. 

Ignore

The axiom will be removed from the axiom list and not be used in the proof. 

Set KITP prover options?

If the user is happy with the current prover settings, which are either the default or those selected after choosing the item Set Specware Proof Options earlier (), select No here.