The envisaged framework consist in a full-fledged inferential apparatus, where the inferential activity can be seen as decomposed into two steps. First, a translation phase brings from one (propositional) modal formalization of a problem to its relational formulation. Then, a deductive method is exploited, within the relational context, in order to seek for a proof.
This paper is devoted to the first of these steps: we describe a prototypical implementation of a Prolog-based tool able to uniformly translate from various modal logics to the calculus of dyadic relations .
The adoption of a declarative programming approach allows us to develop the system in an incremental way and ensures high modularity and extensibility of the application.
At the moment the Prolog translator is able to produce relational rendering of several modal logics (cf. Section 2). We verified that our approach offers an high degree of uniformity: we were able to treat varied modal logics by the very same machinery. Moreover, extensions to further classes of logics can easily be obtained by conservatively adding suitable Prolog clauses.
Possible extensions of the tool are currently under design and development.