---
title: "A Correspondence Theory for Terminological Logics: Preliminary Report"
authors:
  - "Klaus Schild"
doi: ""
url: "https://ijcai.org/proceedings/1991/70"
pdf: "https://ijcai.org/proceedings/1991/0070.pdf"
venue: "Proceedings of the Twelfth International Joint Conference on Artificial Intelligence"
year: 1991
pages: "466-470"
track: "Knowledge Representation"
keywords:
---

# A Correspondence Theory for Terminological Logics: Preliminary Report

Klaus Schild

*Proceedings of the Twelfth International Joint Conference on Artificial Intelligence*, pages 466-470.

## 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 .