Logic with knowledge operator
, subject to
this translation rule:
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.
The translation of intuitionistic logic is based on the following rules:
where is a reflexive and transitive relation.
These logics correspond to multi-modal frames consisting in
a relational system
a family of accessibility relations (enjoying closure properties
with respect to relational constructs).
Modalities are then of the form and
is any relational term of
Other modal logics.
Other modal logics currently accepted by the translator involve:
specification operators, temporal operators, Humberstone operators, sufficiency operators, etc .
As concerns the target language to which the translation is directed, currently
all translation are performed into the algebra of dyadic relations .
So, given a formula the system produces a relational equation of the
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 ;
Output in terms of LATEX commands (for both input and output formulas);