A Correspondence Theory for Terminological Logics: Preliminary Report

Abstract

We show that the terminological logic A.CC 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 A.CC and give a simple proof that subsumption in A.CC is PSPACE-complete, replacing the original six-page one. Furthermore, we consider an extension of A.CC additionally containing both the identity role and the composition, union, transitive-reflexive closure, rang e restriction, and inverse of roles. It turns out that this language, called T S.C , is a notational variant of the propositional dynamic logic converse-PDL. Using this correspondence, we prove that it suffices to consider finite T S.Cmodels, show that T S.C-subsumption is decidable, and obtain an axiomatization ofT S.C. By discovering that features correspond to deterministic programs in dynamic logic, we show that adding them to T S.C preserves decidability, although violates its finite model property. Additionally, we describe an algorithm for deciding the coherence of inverse-free T S.Cconcepts with features. Finally, we prove that universal implications can be expressed within TS.C .