Datensatz

Zusammenfassung

A general framework for translating logical formulae from one logic into \u000Aanother logic is presented. The framework is instantiated with two different \u000Aapproaches to translating modal logic formulae into predicate logic. The first \u000Aone, the well known relational translation makes the modal logic's possible \u000Aworlds structure explicit by introducing a distinguished predicate symbol to \u000Arepresent the accessibility relation. In the second approach, the functional \u000Atranslation method, paths in the possible worlds structure are represented by \u000Acompositions of functions which map worlds to accessible worlds. On the \u000Asyntactic level this means that every flexible symbol is parametrized with \u000Aparticular terms denoting whole paths from the initial world to the actual \u000Aworld. The target logic for the translation is a first‐order many‐sorted logic \u000Awith built in equality. Therefore the source logic may also be first‐order \u000Amany‐sorted with built in equality. Furthermore flexible function symbols are \u000Aallowed. The modal operators \u000Amay be parametrized with arbitrary terms and particular properties of the \u000Aaccessibility relation may be specified within the logic itself.