The system is still at a prototypical stage of development
and most of the features described in the previous sections
are constantly subject of ameliorations.
In particular, we are currently interested in
improving the translation process by enriching and
refining the set of rewriting rules which, at the moment, are largely
realized through syntactical rewriting rules.
Next goal would consist in enhancing the translation process
by improving the capability of exploiting semantic properties of
connectives and constructs;
In connection with the previous point:
improving the capabilities of the translator by extending the
classes of logics it can successfully treat;
Improving the user interface adding more features and control on the input/output and on the
Exploring the possibilities offered by
integration with/within other tools for translation and deduction.
At present time, we are integrating into transIt
a basic graphical proof assistant
based on Rasiowa-Sikorski rewriting rules .
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.
shows a simple example of
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:
(semi-)automated reasoning capabilities;
Exploitation, in the derivation process,
of specific rewriting rules, depending
on the particular logic of the theorem being proved.
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 ).