Created on March 9, 2013, 8:44 p.m. by Hevok & updated by Hevok on May 2, 2013, 5:31 p.m.

To define a model-theoretic Semantic for ALC the Entailment will be define via an Interpretation. An Interpretation is always a Domain, which is a Set of Individuals and an Interpretation Function. The Interpretation Function I maps Individual Names to Domain Elements and it maps Class Names to a Set of Domain Elements, because a Class is a Set of these Elements and it maps Role names to pairs of Domain Elements.

Individuals make up the Domain. Individual Individuals are inside the Domain. Names of Individuals are mapped to individuals in our domain of Interest. Class names are sets of individuals in this Domain. Role names are Pairs of Individuals that are connected via Roles.

With the model-theoretic semantic one tries to go back to a Set Theory view of our Logic.

One also needs an Interpretation of an universal Class/Top Class which is of course the entire universe of the Domain, while the Bottom Class is the Empty Set. The Disjunction and Conjunction. The Interpretation of the Disjunction of two Classes is the Interpretation of a Class combined or union with the Interpretation of another Class. The same holds for the Intersection, so the Conjunction is equal to the Intersection of the Interpretation of the Classes. The Interpretation of a Class C by considering our universe/Domain is without all elements that belong to C. For the universal Quantification one considers all Elements of our Domain for which they are connected a Individual a via the Role R with another individual b. For all the individual b it holds that they belong to the Class C. For the existential Quantifier one considers that there exists an Individual b in that Role or Relation that belongs to the class C and there can also be other Individuals of other Classes.

In the Axioms of the ABox, if one tries to interpret Class membership of a, i.e. a belongs to C, this is only the case if the Interpretation of a belongs to the Set which is the Interpretation of C. The same is for the Role that connects Individuals a and b, which only holds if a and b both belong to the Set of this Pairs of Elements that are the Interpretation of Role R. In the Subsumption C is subsumed by D only then if the Interpretation of C is a Subclass of the Interpretation of D. Equivalently for the Equivalence where the tow Interpretations must be the same.

  • We define a model-theoretic Semantic for ALC (i.e. Entailment will be defined via Interpretations(
  • an Interpretation I=(ΔI,.I) contains
  • a set ΔI (Domain) of Individuals and
  • an interpretation function .I that maps
  • Extension for complex Classes:
  • ⊤I = ΔI and ⊥I = ∅
  • (C ⊔ D)I = CI ∪ DI and (C ⊓ D)I = CI ∩ DI
  • (¬C) = ΔI / CI
  • ∀R.C={a∈ΔI|(∀b∈ΔI)((a,b)∈RI→b∈CI)}
  • ∃R.C={a∈ΔI|(∃b∈ΔI)((a,b)∈RI∧b∈CI)}
  • Axioms
  • C(a) holds, if aI ∈ CI
  • R(a,b) holds, if (aI,bI) ∈ RI
  • C ⊑ D holds, if CI ⊆ DI
  • C ≡ D holds, if Ci = DI

With this model-theoretic Semantic one can doe Reasoning on it.


Tags: semantic, domain, class, interpreting
Categories: Concept
Parent: Description Logics

Update entry (Admin) | See changes

Comment on This Data Unit