The AutoProver

The AutoProver 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 using in-built tactics and a standard library of mathematical laws.

Some obligations may not be proved by the AutoProver. This may be because an obligation is not provable (i.e. there is a mistake in a specification/refinement/implementation), or because the AutoProver's tactics or standard library are inadequate for the proof. In order to supplement the library with additional mathematical laws and/or different tactics, an InterProver session is required.

It is stressed that the InterProver is a BROWSING tool (no `proofs' are committed to the system) which facilitates the inspection of the points at which the AutoProver failed in its attempts to discharge a proof obligation. It enables you to supplement the AutoProver's standard in-built library of mathematical laws with additional laws of your own through the user's PROOFMETHOD file.

Thus different `Levels' of AutoProof are possible, allowing the user to concentrate on different proof obligations at each one, if required; at each Level, the following may be set through the PROOFMETHOD:-

the proof obligations to attempt

the level of forward reasoning depth that the AutoProver should use

the user-supplied theory

the user-supplied tactic

The AutoProver-InterProver cycle has the following structure:

           --> AutoProver
          |        |
          |        |
          |        |                No
          |    POs remaining ?  ---------->  Finished
          |        |
          |        | Yes
          |        |
           <-- InterProver

At each level, the AutoProver's input is a proof obligation file and PROOFMETHOD file (for example at Level 1 `fifi.mch.1.po' and `fifi.mch.1.pmd'); its output is an updated proof obligation file `fifi.mch.2.po' and a template proof obligation file `fifi.mch.2.pmd' (if the latter does not already exist in the PMD, and there remain undischarged proof obligations). This is the used in investigation of the undischarged proof obligations through the next InterProver, session, and subsequent use by the AutoProver at the next level.

During the AutoProof the status of each obligation is represented by a single character as follows:

     p      indicating it has already been discharged 
            at a previous proof level

     .      indicating it is not being attempted at this level 
            (see the ON clause of the PROOFMETHOD)

     +      indicating that it was successfully discharged at this level

     -      indicating that it was attempted but not discharged at this                    level

The current number of outstanding proof obligations and total number of proof obligations (where applicable) is displayed for each construct in the Constructs Area of the Provers Environment panel under `pob' and `tot' respectively.