The source and the target frameworks

Let us start by illustrating most of the source languages currently accepted by the translator. The translation of each of them is actually based on specific transformation rules.

Mono-modal logics.

This is the basic translation of modal formulas into relational terms originated in [11]:

$t(p_i)\;\;=\!\!_{\mbox{\tiny Def}}\;\; p_i'\:;\:{\tt 1}\!\!{\tt l}$,  where $p_i'$ is a relational variable uniquely corresponding to $p_i$, for every propositional variable $p_i$;

$t(\neg \psi)\;\;=\!\!_{\mbox{\tiny Def}}\;\;\overline{t(\psi)}$,  for every propositional sentence $\psi$;

$t(\psi\:{\&}\:\chi)\;\;=\!\!_{\mbox{\tiny Def}}\;\; t(\psi)\:\mbox{\boldmath $\cdot$}\:t(\chi)$,  for all propositional sentences $\psi,\chi$;

$t(\lozenge\:\psi)\;\;=\!\!_{\mbox{\tiny Def}}\;\;\mathsf{r} ; t(\psi)$,  where $\mathsf{r}$ is a constant relation designating the accessibility relation between possible worlds, for every propositional sentence $\psi$.

Lattice-based modal logics.

These logics, together with their corresponding relational renderings, are described in [14,3,9]. The Prolog translator can handle the modal constructs of

-

lattice-based modal logics with possibility operators;

-

lattice-based modal logics with necessity operators;

-

lattice-based modal logics with sufficiency operators.

Logics of knowledge and information.

These modal logics comes from [2]:

-

Logic with knowledge operator $\mathbf{K}$, subject to this translation rule:

$$t(\mathbf{K}\varphi)\;\;=\!\!_{\mbox{\tiny Def}}\;\;\overline{\ma... ...line{t(\varphi)}} \mbox{\boldmath $\cup$} \overline{\mathsf{r};{t(\varphi)}}$$

-

Logic of non-deterministic information (NIL) [2, Sect. 7.2]. A multi-modal logic with three modalities, representing the relation of inclusion and similarity, proper of an information system.

-

Information logic (IL) [2, Sect. 7.3]. A modal logic with three modal operators corresponding to the relations of indiscernibility, forward inclusion, and similarity of an information system.

Intuitionistic logic.

The translation of intuitionistic logic is based on the following rules:

$t(\psi\:{\rightarrow}\:\chi)\;\;=\!\!_{\mbox{\tiny Def}}\;\;\overline{\leqslant;(t(\psi)\:\mbox{\boldmath $\cdot$}\:\overline{t(\chi)})}$

$t(\neg \psi)\;\;=\!\!_{\mbox{\tiny Def}}\;\;\overline{\leqslant;t(\psi)}$

$t(\psi\:{\&}\:\chi)\;\;=\!\!_{\mbox{\tiny Def}}\;\; t(\psi)\:\mbox{\boldmath $\cdot$}\:t(\chi)$

$t(\psi\:{\vee}\:\chi)\;\;=\!\!_{\mbox{\tiny Def}}\;\;t(\psi)\:\mbox{\boldmath $\cup$}\:t(\chi)$

where $\leqslant$ is a reflexive and transitive relation.

Multi-modal logic.

These logics correspond to multi-modal frames consisting in a relational system $(W,\mathit{Rel})$ where $\mathit{Rel}$ is a family of accessibility relations (enjoying closure properties with respect to relational constructs). Modalities are then of the form $[R]$ and $\langle{R}\rangle$ where $R$ is any relational term of $\mathit{Rel}$.

Other modal logics.

Other modal logics currently accepted by the translator involve: specification operators, temporal operators, Humberstone operators, sufficiency operators, etc [12].

As concerns the target language to which the translation is directed, currently all translation are performed into the algebra of dyadic relations [16]. So, given a formula $\varphi$ the system produces a relational equation of the form $t(\varphi)$=${\tt 1}\!\!{\tt l}$.

Further target languages can be easily added by providing suitable description of the languages in terms or rewriting rules. For instance, at the present time, the following targets are under consideration:

• Automated generation of an input file to be processed by deduction systems for relational frameworks. A viable possibility, among others, consists in exploiting a first order theorem prover following the approach described in [6,7];
• Translation into a first order language suitable to be processed by existing deduction systems a la Rasiowa-Sikorski;
• Translation into the language of the theory of aggregates described in [4,1]. In this case, the result of the translation could be inputted to a deduction system for theory-based reasoning [8];
• Output in terms of L^ATEX commands (for both input and output formulas);