At present time, we are integrating into transIt a basic graphical proof assistant based on Rasiowa-Sikorski rewriting rules [13]. Once the user has obtained a relational rendering of a theorem (belonging to one of the various logics acceptable by the translation phase), he can proceed trying to build a proof-tree of the relational translation.
Figure 3 shows a simple example of derivation tree. The user interacts with the system by simply choosing a node of the tree in order to apply one of the rewriting rules. For the time being, the system only takes care of verifying applicability of rules, performing the extension of the tree, and checking if, as a consequence of rule applications, any branch becomes closed.
Envisaged improvements in this context, include:
A further long-term activity regards the integration with visual-oriented tools for manipulation of relational formulas, (based, for instance, on graphical representation of relational expressions and on graph-rewriting techniques [5]).