A formal definition for the expressive power of terminological knowledge representation languages

The notions 'expressive power' or 'expressiveness' of knowledge representation languages (KR languages) can be found in most papers on knowledge representation; but these terms are usually just employed in an intuitive sense. The papers contain only informal descriptions of what is meant by expressiveness. There are several reasons that speak in favour of a formal definition of expressiveness: for example, if we want to show that certain expressions in one language cannot be expressed in another language, we need a strict formalism that can be used in mathematical proofs. Even though we shall only consider terminological KR languages-i.e. KR languages descending from the original system KL-ONE-in our motivation and in the examples, the definition of expressive power that will be given in this paper can be used for all KR languages with Tarski-style model-theoretic semantics. This definition will shed a new light on the tradeoff between expressiveness of a representation language and its computational tractability. There are KR languages with identical expressive power, but different complexity results for reasoning, which comes from the fact that sometimes the tradeoff lies between convenience and computational tractability. The definition of expressive power will be applied to compare various terminological KR languages known from the literature with respect to their expressiveness. This will yield examples for how to utilize the definition both in positive proofs-that is, proofs where it is shown that one language can be expressed by another language-and, more interestingly, in negative proofs-which show that a given language cannot be expressed by the other language.