Proof Assistant Selection

The proof assistant selected for use is Isabelle. It was chosen for a number of reasons:

1. It is general (applicable to a wide range of logics).
2. It is used widely.
3. Work has begun to isolate the intricacies of the system from the logical statements being formed (See: §4.6.)
4. Graphical user interfaces exist, but have so far been targeted mostly at expert users.