A Correspondence Theory for Terminological Logics: Preliminary Report

Abstract

We show that the terminological logic ALC comprising Boolean operations on concepts and value restrictions is a notational variant of the propositional modal logic K_(_m_). To demonstrate the utility of the correspondence, we give two of its immediate by-products. Namely, we axiomatize ACC and give a simple proof that subsumption in ALC is PSPACE-complete, replacing the original six-page one. Furthermore, we consider an extension of ALC additionally containing both the identity role and the composition, union, transitive-reflexive closure, range restriction, and inverse of roles. It turns out that this language, called TSL, is a notational variant of the propositional dynamic logic converse-PDL. Using this correspondence, we prove that it suffices to consider finite TSL-models, show that TSL-subsumption is decidable, and obtain an axiomatization of TSL. By discovering that features correspond to deterministic programs in dynamic logic, we show that adding them to TSL preserves decidability, although violates its finite model property. Additionally, we describe an algorithm for deciding the coherence of inverse-free TSL-concepts with features. Finally, we prove that universal implications can be expressed within TSL. (orig.)