On reductions for multi-modal logics

Abstract

In dieser Arbeit werden mehrere Reduktionen im Zusammenhang mit multimodalen Erweiterungen der wohlbekannten Modallogik K betrachtet, wobei unter einer Reduktion eine Transformation im üblichen komplexitätstheoretischen Sinn verstanden wird. Insbesondere werden Reduktionen zwischen Erfüllbarkeitsproblemen einiger bekannter Logiken besprochen. Ein wesentliches Resultat dieser Arbeit ist eine Transformation von multimodalem K ins herkömmliche K, welche eine Verallgemeinerung einer bestehenden Transformation von bimodalem K ins gewöhnliche K darstellt. Durch die Verknüpfung dieser neuen Reduktion mit einer weiteren bestehenden von K in quantifizierte Aussagenlogik wird eine weitere Übersetzung von multimodalem K in quantifizierte Aussagenlogik erhalten. Umgekehrt wird auf Basis eines klassischen Resultats auch eine Reduktion von quantifizierter Aussagenlogik nach K untersucht. Darüber hinaus wird eine Übersetzung von der prototypischen Beschreibungslogik ALC, die mit multimodalem K nahe verwandt ist, ins herkömmliche K betrachtet. Die vorliegende Arbeit bringt diese unterschiedlichen Ergebnisse in einen einheitlichen Rahmen und eine einheitliche Notation, stellt Details und Beweise bereit, von denen in den ursprünglichen Resultaten viele übersprungen werden, und stellt damit im Wesentlichen eine in sich geschlossene Erörterung dar. Unterstützende Ergebnisse, die für die wesentlichen Resultate relevant sind, aber vor dem Hintergrund der Modallogik gewiss auch für sich genommen von Interesse sind, umfassen eine korrekte und vollständige Axiomatisierung von multimodalem K sowie die endliche Baummodelleigenschaft von K.

In this thesis, several reductions associated with multi-modal extensions of the well-known modal logic K are considered, where by a reduction is understood a transformation in the usual complexity-theoretical sense. In particular, reductions between satisfiability problems of some well-known logics are discussed. Generalizing an existing translation from bimodal K to standard K, a central result of this thesis is a reduction from arbitrary multi-modal K to standard K. Combining this new reduction with another existing one from K to quantified propositional logic, a further translation from multi-modal K to quantified propositional logic is obtained. Conversely, based on a classical result, also a reduction from quantified propositional logic to K is examined. Moreover, a transformation from the prototypical description logic ALC, which is closely related to multi-modal K, to standard K is considered. The present thesis brings these different considered outcomes into a uniform setting and notation, provides details and proofs many of which are omitted in the original results, and thus constitutes an essentially self-contained exposition. Auxiliary outcomes which are relevant for the central results, but are certainly also of interest in their own right, in the light of modal logic, include a sound and complete axiomatization for multi-modal K, and the finite-tree model property of K.