The BToolProver

The BToolProver is invoked from the Provers Environment:

It is applicable to all machines, refinements, and implementations, which are pogenerated, and currently have undischarged proof obligations.

It is a tool which attempts to discharge the proof obligations generated by the POGenerator through a tailored graphical interface, giving the user absolute control at each step of the proof. User theory may be supplied, and the system library of mathematical rules inspected.

Upon invocation of the BToolProver, you are presented with the Main Menu:

See figure

It is possible to edit/reload the current or global PROOFMETHOD used in the AutoProver and InterProver, but a separate body of rules may be used in the BToolProver (rules which would not necessarily be appropriate for automated proof). It is also possible to view the entire mathematical library of rules available to all three provers, for example:

See figure

In the Main window, you are presented with a list of theories containing outstanding proof obligations, each may be selected (by `clicking') and proved (a toggle may be set on the Theory Menu window to display just those rules which are unproved).

See figure

When a rule is selected, the Forward Reasoning Depth and FEQL may be set before proof commences:

Note

The Forward Tactic is set from that in the current PROOFMETHOD; foward library theories are added to the tactic appropriate to the Forward Reasoning Depth set.

See figure

At each step of the proof, a context-sensitive menu is provided showing what is possible at the current step (non-applicable options are desensitised) and the proof tree displayed in graphical form, showing the manner in which the proof has been constructed so far, with the rules applied at each step:

See figure See figure

Applicable rules may be selected by `clicking', and hypotheses of any branch of the tree may also be inspected and filtered:

See figure See figure

It is possible to `Undo' each step of the proof, and try to construct it in a different manner.

Lemmas may also be created at any stage of the proof (they are added to a theory called `BToolLemmas'), and may be proved later in the same BToolProver session, or in a higher-level proof session; lemmas thus created are available in the proofs of other outstanding obligations.