Set Prover Display Options

      In this section we discuss how to control the way in which KITP interacts with the user and displays successful proofs or failed proof attempts. Setting of these parameters results from selecting the item of the same name, Set Prover Display Options from the menu entitled Select an Operation (). The following alternatives appear:

Suppress KITP Message?

  Choosing Yes means the user does not want to see any messages from the Specware theorem prover. This is a bad-tempered and unfriendly choice. KITP works hard to prepare those messages.  Nevertheless, the default is Yes.

Display Proof Object?

  The proof object is what is passed to the theorem prover before the proof begins. It consists of the axiom list and the conjecture. Because KITP is a refutation procedure, the conjecture will be negated. The default is Cnj, meaning conjecture only. Obj means the entire proof object. None means neither.

Select Witnesses by:

  This refers to the answer-extraction  capability of KITP, which is not used in this version of Specware. Leave it on the default, which is Prover.

Display Input Clauses?

  The input clauses correspond to the axiom list, those consequences generated in the forward inference phase, and the negated conjecture. The input clauses are what is passed to the backward inference phase. The default is No.

Display Sort Axioms?

   Sort axioms describe the operations that construct and deconstruct sorts. Note that even if you choose Yes, no sort axioms will be displayed unless you also choose Yes for the previous option, Display Input Clauses. Frequently, we want to see all the axioms except the sort axioms, which are automatically generated. The default is No.

Forward Interact?

  Will the forward inference phase require detailed user guidance? The default is No.

Display Forward Derivation?

  Should the consequences generated during the forward inference phase be displayed? If Yes is selected, all derived consequences will be displayed, whether or not a proof is ultimately found or those consequences take part in the proof. The default is No.

Backward Interact?

  Will the backward inference phase require detailed user guidance? The default is No.

Display Backward Derivations?

  Would the user like to see the details of the backward-derivation phase? This will include all consequences obtained, whether or not the proof succeeds or the results are relevant to the proof. The default is No.

Display Proof Tree?

  If the proof succeeds, would the user like to see it? Only clauses relevant to the proof will be displayed. The default is Yes.

Display Type Constraints?

   Should the display of the proof include type information (e.g., x : integer). If so, select Yes, which is the default.

Ignore Data Types?

  Whether or not typed inference is employed, KITP normally adheres to type restrictions; this corresponds to the default, No. If it is suspected that type restrictions are causing a proof to fail, choose Yes to attempt the proof without type restrictions. Be careful not to regard the conjecture as proved, however, unless the proof succeeds with type restrictions.

Ask on Failure?

  When a proof fails, the user is asked whether to try again, if Yes is selected. The default is No.