Set Specware Proof Options

  

This is one of the options offered under the toolbar item Prover Options ().

In this section, we discuss the setting of the parameters that control the Specware theorem prover, KITP  (). A separate section describes the control of the way in which KITP displays proof attempts.

Certain of the parameters control the answer-extraction  feature of KITP. This feature allows information, other than the validity of a conjecture, to be obtained by systematic analysis of the proof. Because this feature is not exploited in the current version of Specware, we shall not describe the meaning of the settings. In all cases the default can be retained.

      Setting of the parameters can be invoked by selecting the item Set Specware Proof Options from the menu entitled Select an Operation. It also can also result from selecting the item Display/modify Specware Proof Options from the same menu, but then the choice will be deferred until a proof is actually attempted.

When the parameters are to be set, a menu headed Set New Values for Prover (Kitp) Parameters   with the following items appears:  

Conjectures to Focus.

  This option does not apply to normal Specware use--leave it on the default (All).

Search Strategy.

   Leave this on the default (O-F). 

Use Typed Inference.

   Normally for Specware, KITP uses a typed inference restriction, in which each term has a type (e.g., x : integer) and unification is not permitted across types; this corresponds to the choice Yes, which is the default. Choose No only if it is believed that the typing is causing the proof to fail; this will cause KITP to abandon type inference and represent types instead by predicates (e.g., (typeof x integer)).

Assume Hypothesis Consistent?

  If Yes, no attempt will be made during the backward inference phase to find a contradiction between the hypotheses of the theorem and the other axioms; this will restrict the search space. Otherwise, the hypotheses are treated as goals, just like the conclusions of the theorem; if a contradiction is discovered, the theorem holds vacuously, and the proof is complete. (In other words, the hypothesis will be included in the set of support.) No is the default.  

Include Sort Axioms?

   Are the sort axioms to be included in the axiom list? If they are unnecessary, omitting them will reduce the search space. The default is Yes, sort axioms are included.

Use Free Paramodulation?

    This is a form of paramodulation in which a variable x can be replaced by a term t. Because it is very explosive, it is usually outlawed; this corresponds to the default, No.

Maximum Input Clauses.

  This sets a limit to the total number of clauses that make up the input to the backward inference phase . This includes clauses corresponding to the axiom list and the conjecture, and any clauses derived during the forward inference phase. The default is 1000.

Generic Forward Inference?

   There are two subphases of forward inference. In generic forward inference, KITP reasons from axioms but ignores hypotheses and goals altogether. A No (the default) indicates that this phase is to be omitted. This is preferred because usually the most useful consequences of the axioms are already included as conjectures.

In ordinary forward inference, which is performed regardless of the selection here, KITP reasons forward from hypotheses and other axioms (including any generated by generic forward inference). In this second subphase, however, all consequences must be derived, directly or indirectly, from a hypothesis.

Forward Depth Limit.

  This setting limits the depth of the inferences that may be performed in the forward inference phase. Depth 1 clauses are derived from the axioms in one step; depth 2 clauses are derived from axioms and depth 1 clauses in one step, and so on. The default maximum depth is 2.

Forward Derivation Limit.

  This setting limits the number of new clauses that may be generated during the forward inference phase of a given conjecture. The default is 100.

Backward Depth Limit.

  The backward inference phase (BIP) reasons backwards from the the goals, unit clauses, and axioms that have been earmarked for backwards inference. The Backward Depth Limit setting limits the depth of the inferences that may be performed during the BIP of a given conjecture. The default is 5. (See Forward Depth Limit for more explanation.)

Backward Derivation Limit.

  This setting limits the number of new clauses that may be generated during the backward inference phase of a given conjecture. The default is 3000.

Forward Fnsnest Limit.

  This setting limits the depth of function nesting for terms in clauses generated during the forward inference phase. For example, (g (f a b) (f c d)) has depth 2 but (h (g (f a b) c)) has depth 3. The default is 2.

Maximum New Variables.

  Limits the number of variables that may be introduced into a new clause during the backward inference phase, other than those that already appear in the goal from which it was deduced. The default is 5.

Minimum Witnesses Deduced.

   This pertains to the answer-extraction feature of the theorem-prover, which is not exploited in this version of Specware.

Return Value when Fail.

  If the theorem prover fails to find a proof, the setting determines the course of action: False and True means the conjecture is treated as if it is false and true, respectively; Ask means the user is queried after the failure to decided on each conjecture individually. We may leave this on the default, false. If we want to accept conjectures as theorems without proof, we may use an earlier option, When prover fails, query user to accept theorems anyway? ().

Choice of Dump Proofs.

   Which KITP proofs should be dumped into the selected directory ()? Select Failed if only failed proofs should be saved; otherwise, select All or None.

Ask when Dump Proof?

  Should KITP ask the user before it attempts to save a proof? The default is No. Note that, if Yes is selected, the user will not be asked about proofs that have been excluded under the previous option, Choice of Dump Proofs.

Enforce Strong Dependency?

  This refers to the answer-extraction  feature of KITP.