Specware contains a built-in resolution theorem prover, KITP . In invoking KITP, the conjecture is negated, and axioms and conjecture are translated into clausal form. Resolution , paramodulation , and rewriting operations are applied to the resulting clauses, in an attempt to derive a contradiction.
KITP distinguishes between two phases, a forward inference phase (FIP), in which consequences are derived from the axioms and the hypotheses (if any) of the conjecture, and a backward inference phase (BIP), in which consequences are derived that involve the conclusion of the conjecture as well. The FIP is strictly limited in power; for instance, only unit axioms and hypotheses, and implication axioms, are used. In the BIP, axioms of any form, hypotheses, and goals are used.
KITP also has a rewriting (simplification) phase, in which subterms of KITP expressions are replaced by simpler but semantically equivalent terms. Any consequence derived by KITP is subjected to simplification. Selected axioms that are in the form of equalities may be used as simplification rules.
Some guidance to the theorem prover can be given before any proof is
attempted, that is, before we parse or verify any specification or
specification morphism. In this section, we say what controls there
are. Later
(
), we
give examples that illustrate the use of these controls. The reader
may prefer to head directly to the examples and refer back to this
section as necessary.
The main window frame of the Specware window interface includes a toolbar of five items, just below the title bar. Three of these are relevant to the control of the theorem prover, and may be selected by mouse clicks.
General Information about Menus: All selections are made with the left-most mouse button, unless specified otherwise. The selected item will be highlighted in reverse, as white letters on a black background. Most Specware menus appear with a number of options, including Do It and Abort . After making satisfactory selections, the user selects Do It. If it is decided that no new selections need to be made after all, the user may select Abort.