Dr. Hans Jürgen Ohlbach

Selected Publications about Translation Methods for Non-Classical Logics

Encoding two-valued non-classical logics in classical logic
Hans Jürgen Ohlbach, Andreas Nonnengart, Maarten de Rijke and Dov Gabbay

This paper will appear in the Handbook of Automated Reasoning

uncompressed files PostScript (1.0M) PDF (751K)
compressed files PostScript (257K) PDF (559K)

Functional Translation and Second-Order Frame Properties of Modal Logics
Hans Jürgen Ohlbach and Renate Schmidt

Normal modal logics can be defined axiomatically as Hilbert systems, or semantically in terms of Kripke's possible worlds and accessibility relations. Unfortunately there are Hilbert axioms which do not have corresponding first-order properties for the accessibility relation. For these logics the standard semantics-based theorem proving techniques, in particular, the relational translation into first-order predicate logic, do not work. There is an alternative translation, the so-called functional translation, in which the accessibility relations are replaced by certain terms which intuitively can be seen as functions mapping worlds to accessible worlds. In this paper we show that from a certain point of view this functional language is more expressive than the relational language, and that certain second-order frame properties can be mapped to first-order formulae expressed in the functional language. Moreover, we show how these formulae can be computed automatically from the Hilbert axioms. This extends the applicability of the functional translation method.

uncompressed files dvi (176K) PostScript (382K) PDF ([an error occurred while processing this directive]) bib
compressed files dvi ( 45K) PostScript ( 94K) PDF ([an error occurred while processing this directive])

Translating Graded Modalities into Predicate Logic
Hans Jürgen Ohlbach, Renate Schmidt and Ullrich Hustadt

In the logic of graded modalities it is possible to talk about sets of finite cardinality. Various calculi exist for graded modal logics and all generate vast amounts of case distinctions. In this paper we present an optimized translation from graded modal logic into many-sorted predicate logic. This translation has the advantage that in contrast to known approaches our calculus enables us to reason with cardinalities of sets symbolically. In many cases the length of proofs for theorems of this calculus is independent of the cardinalities. The translation is sound and complete.

uncompressed files dvi (181K) PostScript (450K) PDF (458K) bib
compressed files dvi ( 61K) PostScript (157K) PDF (343K)

Translation Methods for Non-Classical Logics -- An Overview
Hans Jürgen Ohlbach

This paper gives an overview on translation methods we have developed for nonclassical logics, in particular for modal logics. Optimized `functional' and semi-functional translation into predicate logic is described. Using normal modal logic as an intermediate logic, other logics can be translated into predicate logic as well. As an example, the translation of modal logic of graded modalities is sketched. In the second part of the paper it is shown how to translate Hilbert axioms into properties of the semantic structure and vice versa, i.e. we can automate important parts of correspondence theory. The exact formalisms and the soundness and completeness proofs can be found in the original papers.

uncompressed files dvi ( 91K) PostScript (285K) PDF (181K) bib
compressed files dvi ( 37K) PostScript (110K) PDF (162K)

Semantics Based Translation Methods for Modal Logics
Hans Jürgen Ohlbach

A general framework for translating logical formulae from one logic into another logic is presented. The framework is instantiated with two different approaches to translating modal logic formulae into predicate logic. The first one, the well known relational translation makes the modal logic's possible worlds structure explicit by introducing a distinguished predicate symbol to represent the accessibility relation. In the second approach, the functional translation method, paths in the possible worlds structure are represented by compositions of functions which map worlds to accessible worlds. On the syntactic level this means that every flexible symbol is parametrized with particular terms denoting whole paths from the initial world to the actual world. The ``target logic'' for the translation is a first-order many-sorted logic with built in equality. Therefore the ``source logic'' may also be first-order many-sorted with built in equality. Furthermore flexible function symbols are allowed. The modal operators may be parametrized with arbitrary terms and particular properties of the accessibility relation may be specified within the logic itself.

uncompressed files PostScript (1.0M) PDF (215K) bib
compressed files PostScript (169K) PDF (196K)

Last Modified: Wednesday, 02-Aug-2000 14:18:56 CEST