Identifiers

The Web Ontology Language uses QNames as names.
N is the set of all QNames.
The Web Ontology Language QNames should be taken as abbreviations for URIs plus fragments.

Datatypes

A datatyping scheme is a collection of datatypes, DT.
For each datatype d in DT there are four components:

	U(d), the QName for the datatype;
	L(d), the lexical space for the datatype;
	V(d), the value space for the datatype; and
	LV(d) : L(d) -> V(d), the lexical-to-value mapping for the datatype.

Datatypes

	L  = union over d in DT of L(d), lexical values
	V  = union over d in DT of V(d), data values
	LV = union over d in DT of LV(d)

Interpretations

A Web Ontology Language interpretation, I, over a datatyping scheme DT consists of

	R, nonempty, disjoint from V	the domain of resources 
	EXT  : N -> 2^(Rx(RuV))		property extensions
	CEXT : N -> 2^R			class extensions
	S    : N -> R			individual denotation function

	CEXT(owl:Thing)	       =  R
	CEXT(owl:Nothing)      =  {}

Denotation of Frame Constructs

  ID(super(c_1,...,c_n)) = ID(c_1) ^ ... ^ ID(c_n)
  ID(slot(prop,range=range,modality,multiplicity,
		required=c_1,...,required=c_n,value=i_1,...,value=i_m)
	= { x : if <x,y> in EXT(prop) then y in ID(range) 
	    and if modality=required then exists y <x,y> in EXT(prop) 
	    and if multiplicity=singlevalued then atmost 1 y <x,y> in EXT(prop)
	    and exists y in CEXT(c_i) with <x,y> in EXT(prop) for 1 <= i <= n
	    and <x,S(i_i)> in EXT(prop) for 1 <= i <= m }
  ID(slot(prop,datatypeRange,modality,multiplicity,
		required=d_1,...,required=d_n,value=dv_1,l_1,...,value=dv_m,l_m)
	= [ as above ]

Denotation of Descriptions

  ID(class) 			= CEXT(class)
  ID(unionOf(d1,...,dn))	= ID(d1) v ... v ID(dn)
  ID(intersectionOf(d1,...,dn)) = ID(d1) ^ ... ^ ID(dn)
  ID(complementOf(d))		= R \ ID(d)
  ID(oneOf(i1,...,in))		= { S(i1), ..., S(in) }
  ID(localRange(prop,cd))	= { x : <x,y> in EXT(prop) -> y in IC(cd) }
  ID(required(prop,cd))		= { x : exists y <x,y> in EXT(prop) and 
					y in IC(class) }
  ID(value(prop,id))		= { x : <x,S(id)> in EXT(prop) }
  ID(value(prop,dt,l))		= { x : <x,LV(U-(dt))(l)> in EXT(prop) }

Denotation of Descriptions

  ID(minCardinality(prop,int))  = { x : >=int y  <x,y> in EXT(prop) }
  ID(maxCardinality(prop,int))  = { x : <=int y  <x,y> in EXT(prop) }
  ID(cardinality(prop,int))     = { x : =int y  <x,y> in EXT(prop) }

  IC(oneOf(dt1,l1,...,dtn,ln))	= { LV(dti)(li), ..., LV(dtn)(ln) }
  IC(dt)			= V(U-(dt))	for dt a datatype QName
  IC(c)				= ID(c)		for other QNames

Denotation of Facts

  IP( (property,fact) )       = { r in R: for some r2 in IS(fact) 
					  < r, r2 > in EXT(property) }
  IP( (property,individual) ) = { r in R : < r, S(property) > in EXT(property) }
  IP( (property,dt,l) )       = { r in R : <x,LV(U-(dt))(l)> in EXT(property) }

  IS( Individual(individual,class,pv1,...,pvn) ) = { S(individual) } ^
		{ r in R : r in CEXT(class) and r in IP(pv1) ... r in IP(pvn) }
  IS( Individual(class,pv1,...,pvn) ) =
		{ r in R : r in CEXT(class) and r in IP(pv1) ... r in IP(pvn) }

Satisfaction

An interpretation, I = < R, EXT, CEXT, S >, satisfies a Web Ontology Language KB if it satisfies each definition and fact in the KB.

Satisfaction of Class Definitions

  DefinedClass(class,supers(c_1,...,c_n),s_1,...,s_m)
		CEXT(class) = ID(c_1) ^ ... ^ ID(c_n) ^ ID(s_1) ^ ... ^ ID(s_m)
  PrimitiveClass(class,supers(c_1,...,c_n),s_1,...,s_m)
		CEXT(class) <= ID(c_1) ^ ... ^ ID(c_n) ^ ID(s_1) ^ ... ^ ID(s_m)
  DefinedClass(class,description_1,...,description_n)
		CEXT(class) = ID(description_1) ^ ... ^ ID(description_n)
  PrimitiveClass(class,description_1,...,description_n)
		CEXT(class) <= ID(description_1) ^ ... ^ ID(description_n)
  EnumeratedClass(class,id1,...,idn)
		CEXT(class) = { S(id1), ..., S(idn) }

Satisfaction of Class Definitions

  SameClassAs(description_1,...,description_n)
  		ID(description_i) = ID(description_j) 1 <= i < j <= n
  SubClassOf(description_1,description_2)
  		ID(description_1) <= ID(description_2)
  Disjoint(description_1,,...,description_n)
		ID(description_i) ^ ID(description_j) = {}  1 <= i < j <= n

Satisfaction of Property Definitions

  SamePropertyAs(property_1,property_2)
		EXT(property_1) = EXT(property_2)
  SubPropertyOf(property_1,property_2)
		EXT(property_1) <= EXT(property_2)
  Domain(property,description)
		EXT(property) <= ID(description) x (RuV)
  Range(property,description)
		EXT(property) <= R x IC(description)

Satisfaction of Property Definitions

  SingleValuedProperty(property)
		EXT(property) is functional
  UniquelyIdentifyingProperty(property)
		converse of EXT(property) is functional and 
		EXT(property) <= R x R
  TransitiveProperty(property)
		EXT(property) is transitive and EXT(property) <= R x R

Satisfaction of Facts

  Individual(i,class,pv_1,...,pv_n)
		S(i) in CEXT(class), S(i) in IP(pv1), ..., S(i) in IP(pvn)
  Individual(class,pv1,...,pvn)
		there is some r in R such that 
			r in CEXT(class), r in IP(pv1), ..., r in IP(pvn)

  SameIndividual(individual_1,...,individual_n)
		S(individual_i) = S(individual_j)	1 <= i < j <= n
  DifferentIndividuals(individual_1,...,individual_2)
		S(individual_i) /= S(individual_j)	1 <= i < j <= n

Models and entailment

An interpretation is a model for a Web Ontology Language KB if the interpretation satisfies the KB.

A Web Ontology Language knowledge base, KB1, entails another, KB2, if all models of KB1 are also models of KB2.