English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Journal Article

Semantics Based Translation Methods for Modal Logics

MPS-Authors
/persons/resource/persons45140

Ohlbach,  Hans Jürgen
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available
Citation

Ohlbach, H. J. (1991). Semantics Based Translation Methods for Modal Logics. Journal of Logic and Computation, 1(5), 691-746. doi:10.1093/logcom/1.5.691.


Cite as: https://hdl.handle.net/11858/00-001M-0000-0023-C355-6
Abstract
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.