The B-Tool is a stand-alone Theorem Proving Assistant.

It stores the axioms, rules of inference, lemmas, theorems and proofs
which arise in the process of mathematical reasoning. It provides an
environment for the interactive as well as the automatic construction
of proofs using rules of inference and axioms.

The rules of inference and axioms can be added freely, but their
application in proofs are strongly controlled, preventing common
errors such as unintentional variable capture.

The B-Tool provides a graphical interface to the proof process -
presenting incomplete proofs as trees indicating which rules are
applicable to the 'leaves' of the tree.

A special tailored B-Tool, which incorporates reasoning rules for Set
Theory, is integrated within the B-Toolkit.

The B-Tool provide flexibility as not only the reasoning rules but
also most of the syntax are user defined. This flexibility is
exploited to provide the reasoning mechanisms for AMN inside the
B-Toolkit.