The meaning of a terminology, and of the common inference problems, is given in terms of a Tarski style model theoretic semantics using interpretations [2,6,4]. An interpretation consists of a set , called the abstract domain of , a set , called the concrete domain of , and a valuation function . The abstract and concrete domains must be disjoint, i.e., .
The valuation function maps every concept to a subset of and every role to a subset of ) such that, for all concepts , , roles , , concrete predicate expressions and non-negative integers , the equations in Figure 5 are satisfied (where denotes the cardinality of a set ). Concrete predicate expressions have the obvious interpretation as shown in Figure 6. The ordering on strings is the standard lexicographic one.
The concrete domain is treated differently from the abstract domain because it is considered to be already sufficiently structured by the predicates min, max etc. Therefore, it is not appropriate to form new classes of concrete objects (values) using the concept language .
In order to avoid considering roles such as (i.e., the inverse of an inverse) we will define a function such that is and is . A role is directly subsumed by a role w.r.t. a terminology iff either or . A role is subsumed by a role w.r.t. (written ) iff is directly subsumed by a or there is a role such that is directly subsumed by a and . A role is equivalent to a role w.r.t. (written ) iff and . A role is transitive in iff for some role such that or (this defines , the set of transitive role names). A role is a simple role in iff there is no role such that is transitive in and .
An interpretation satisfies a terminology iff for every axiom in , , for every axiom in , and for every transitive role in , . Such an interpretation is called a model of (written ).
A concept is satisfiable with respect to a terminology (written ) iff there is a model of with . A concept is subsumed by a concept w.r.t. (written ) holds for each model of .
An OIL ontology is called consistent iff . A class in an ontology is called consistent iff . A class is a subclass of a class in an ontology iff .