Providing 4 different but integrated proof tools satisfying the need
to carry out proofs in different manners depending on the nature and
the difficulty of the proof problem; proofs may be attempted at
different `levels' to permit the use of the four proof tools.

• The AutoProver
  

  driven by a tactic and a `ProofMethod', containing the theories
  provided by the user, and controls the depth of `forward reasoning'
  used during the proofs.

• The InterProver
  

  also driven by a tactic and a `ProofMethod', providing an environment
  in which user-provided theory may be introduced; proof proceeds by the
  classical mathematical approach of `lemma-creation', each lemma being
  subsequently proved. A trace of the emerging proof is given to enable
  the user to detect shortcomings in his/her approach.

• The B-Tool prover
  

  driven by the user in a step-by-step manner. During the proof all
  applicable rules from the built in theories are presented and can be
  inspected. Proof-attempts can be made by selecting a valid proof
  step. The proof is build up graphically as a `tree' during the users
  interaction with the prover. The `hypothesis' associated with
  outstanding `goals' can be inspected by `clicking' the leaves of the
  tree and searched for the presence of particular
  expressions. `Lemma-creation' is also employed here, each lemma being
  subsequently proved either by the B-Tool prover, or presented to the
  AutoProver at the next proof level.

• The ProofPrinter
  

  providing proof listings together with rules from the built-in
  mathematical library and any user-provided rules used. Proofs are
  presented in such a way that they can be checked independently by
  another agent.

• A Proof status tool