Last Modified by Carroll based on the published WD
Using this model-theoretic semantics for OWL Lite defines owl-lite-entailment, such whenever A owl-lite-entails B then A owl-entails B (both OWL DL and OWL Full). A specific OWL Lite reasoner MAY find more entailments than this, but MUST not find entailments that are not Owl Full entailments.
OWL Lite is a subset of OWL DL, and the semantics is a minor modification of the OWL DL semantics. The goals are:
Some classic T-Box style problems, such as classification, are non-objectives. A reasoner that supports classification can be OWL Lite conformant, but is not required.
From the RDF model theory [RDF MT], for V a set of URI references containing the RDF and RDFS vocabulary, an RDFS interpretation over V is a triple I = < RI, EXTI, SI >. Here RI is the domain of discourse or universe, i.e., a set that contains the denotations of URI references. EXTI is used to give meaning to properties, and is a mapping from RI to sets of pairs over RI × (RI∪LV). Finally, SI is a mapping from V to RI that takes a URI reference to its denotation. CEXTI is then defined as CEXTI(c) = { x∈RI | <x,c>∈EXTI(SI(rdf:type)) }. RDFS interpretations must meet several conditions, as detailed in the RDFS model theory. For example, SI(rdfs:subClassOf) must be a transitive relation.
An OWL interpretation, I = < RI, EXTI, SI >, over a vocabulary V, where V includes VRDFS, rdfs:Literal, VOWL, owl:Thing, and owl:Nothing, is an RDFS interpretation over V that satisfies the following conditions:
Relationships between OWL classes
| If E is | then CEXTI(SI(E))= | with |
|---|---|---|
| owl:Thing | IOT | IOT⊆RI |
| owl:Nothing | {} | |
| rdfs:Literal | LV | |
| owl:Class | IOC | IOC⊆CEXTI(SI(rdfs:Class)) |
| owl:Restriction | IOR | IOR⊆IOC |
| owl:Datatype | IDC | IDC⊆CEXTI(SI(rdfs:Class)) |
| owl:Property | IOP | IOP⊆CEXTI(SI(rdf:Property)) |
| owl:ObjectProperty | IOOP | IOOP⊆IOP |
| owl:DataTypeProperty | IODP | IODP⊆IOP |
| rdf:List | IL | IL⊆RI |
Membership in OWL classes
| If E is | then SI(E)∈ |
|---|---|
| owl:Thing | IOC |
| owl:Nothing | IOC |
| rdfs:Literal | IDC |
| a datatype of D | IDC |
| rdf:nil | IL |
Characteristics of members of OWL classes
| If E is | then if e∈CEXTI(SI(E)) then |
|---|---|
| owl:Class | CEXTI(e)⊆IOT |
| owl:Datatype | CEXTI(e)⊆LV |
| owl:ObjectProperty | EXTI(e)⊆IOT×IOT |
| owl:DatatypeProperty | EXTI(e)⊆IOT×LV |
The next constraints are IFFIf-Then, which may be harder to deal with in OWL/DL, as they extend the various categories of properties to all of owl:Property. However, in OWL/DL ontologies you can neither state that an owl:DatatypeProperty is inverse functional nor ask whether it is, so there should be not adverse consequences.
| If E is | then if c∈CEXTI(SI(E)) iff then c∈IOP and |
|---|---|
| owl:SymmetricProperty | <x,y> ∈ EXTI(c) → <y, x>∈EXTI(c) |
| owl:FunctionalProperty | <x,y1> and <x,y2> ∈ EXTI(c) → y1 = y2 |
| owl:InverseFunctionalProperty | <x1,y>∈EXTI(c) ∧ <x2,y>∈EXTI(c) → x1 = x2 |
| owl:TransitiveProperty | <x,y>∈EXTI(c) ∧ <y,z>∈EXTI(c) → <x,z>∈EXTI(c) |
RDFS domains and ranges are strengthened to if-and-only-if over the OWL universe.
Some OWL properties have iffif-then characterizations
| If E is | then if <x,y>∈EXTI(SI(E)) iffthen |
|---|---|
| owl:sameClassAs | x,y∈IOC ∧ CEXTI(x)=CEXTI(y) |
| owl:disjointWith | x,y∈IOC ∧ CEXTI(x)∩CEXTI(y)={} |
| owl:samePropertyAs | x,y∈IOP ∧ EXTI(x) = EXTI(y) |
| owl:inverseOf | x,y∈IOOP ∧ <u,v>∈EXTI(x) iff <v,u>∈EXTI(y) |
| owl:sameIndividualAs | x = y |
| owl:sameAs | x = y |
| owl:differentFrom | x ≠ y |
Some OWL properties have only-if characterizations
We will say that l1 is a sequence of
y1,…,yn over C iff
n=0 and l1=SI(rdf:nil)
or n>0 and l1∈IL and
∃ l2, …, ln ∈ IL such that
<l1,y1>∈EXTI(SI(rdf:first)), y1∈CEXTI(C),
<l1,l2>∈EXTI(SI(rdf:rest)), …,
<ln,yn>∈EXTI(SI(rdf:first)), yn∈CEXTI(C), and
<ln,SI(rdf:nil)>∈EXTI(SI(rdf:rest)).
| If E is | then if <x,y>∈EXTI(SI(E)) then |
|---|---|
| owl:complementOf | x,y∈ IOC and CEXTI(x)=IOT-CEXTI(y) |
| If E is | then if <x,l>∈EXTI(SI(E)) then |
|---|---|
| owl:unionOf | x∈IOC and l is a sequence of y1,…yn over IOC and CEXTI(x) = CEXTI(y1)∪…∪CEXTI(yn) |
| owl:intersectionOf | x∈IOC and l is a sequence of y1,…yn over IOC and CEXTI(x) = CEXTI(y1)∩…∩CEXTI(yn) |
| owl:oneOf | x∈CEXTI(rdfs:Class) and l is a sequence of y1,…yn over RI∪LV and CEXTI(x) = {y1,..., yn} |
| If E is | and | then if <x,l>∈EXTI(SI(E)) then |
|---|---|---|
| owl:oneOf | l is a sequence of y1,…yn over LV | x∈IDC and CEXTI(x) = {y1,..., yn} |
| owl:oneOf | l is a sequence of y1,…yn over IOT | x∈IOC and CEXTI(x) = {y1,..., yn} |
Todo: think about oneof
| If | then x∈IOR, y∈IOC, p∈IOP, and CEXTI(x) = |
|---|---|
| <x,y>∈EXTI(SI(owl:allValuesFrom))) ∧ <x,p>∈EXTI(SI(owl:onProperty))) |
{u∈IOT | <u,v>∈EXTI(p) → v∈CEXTI(y) } |
| <x,y>∈EXTI(SI(owl:someValuesFrom))) ∧ <x,p>∈EXTI(SI(owl:onProperty))) |
{u∈IOT | ∃ <u,v>∈EXTI(p) ∧ v∈CEXTI(y) } |
| <x,y>∈EXTI(SI(owl:hasValue))) ∧ <x,p>∈EXTI(SI(owl:onProperty))) |
{u∈IOT | <u, y>∈EXTI(p) } |
| If | then x∈IOR, y∈LV, y is a non-negative integer, p∈IOP, and CEXTI(x) = |
| <x,y>∈EXTI(SI(owl:minCardinality))) ∧ <x,p>∈EXTI(SI(owl:onProperty))) |
{u∈IOT | card({v : <u,v>∈EXTI(p)}) ≥ y } |
| <x,y>∈EXTI(SI(owl:maxCardinality))) ∧ <x,p>∈EXTI(SI(owl:onProperty))) |
{u∈IOT | card({v : <u,v>∈EXTI(p)}) ≤ y } |
| <x,y>∈EXTI(SI(owl:cardinality))) ∧ <x,p>∈EXTI(SI(owl:onProperty))) |
{u∈IOT | card({v : <u,v>∈EXTI(p)}) = y } |
RI contains elements corresponding to all possible OWL descriptions and data ranges
Maybe the comprehension principle on lists should go too. Leaving it in for now.
The first three conditions require the existence of the finite sequences that are used in some OWL constructs. The remaining conditions require the existence of the OWL descriptions and data ranges.
| If there exists | then there exists l1,…,ln ∈ IL with |
|---|---|
| x1, …, xn ∈ IOC | <l1,x1> ∈ EXTI(SI(rdf:first)),
<l1,l2> ∈ EXTI(SI(rdf:rest)), … <ln,xn> ∈ EXTI(SI(rdf:first)), <ln,SI(rdf:nil)> ∈ EXTI(SI(rdf:rest)) |
| x1, …, xn ∈ IOT∪LV | <l1,x1> ∈ EXTI(SI(rdf:first)),
<l1,l2> ∈ EXTI(SI(rdf:rest)), … <ln,xn> ∈ EXTI(SI(rdf:first)), <ln,SI(rdf:nil)> ∈ EXTI(SI(rdf:rest)) |
All of the following comprehension principls go, except possibly that for intersection, my preference is for it to go, too.
| If there exists | then there exists y with |
|---|---|
| l, a sequence of x,…,xn over IOC | y∈IOC, <y,l> ∈ EXTI(SI(owl:unionOf)) |
| l, a sequence of x1,…,xn over IOC | y∈IOC, <y,l> ∈ EXTI(SI(owl:intersectionOf)) |
| l, a sequence of x1,…,xn over IOT∪LV | y∈CEXTI(SI(rdfs:Class)), <y,l> ∈ EXTI(SI(owl:oneOf)) |
| If there exists | then there exists y ∈ IOC with |
| x ∈ IOC | <y,x> ∈ EXTI(SI(owl:complementOf)) |
| If there exists | then there exists y ∈ IOR with |
| x ∈ IOP ∧ w ∈ IOC ∪ IDC | <y,x> ∈ EXTI(SI(owl:onProperty)) ∧ <y,w> ∈ EXTI(SI(owl:allValuesFrom)) |
| x ∈ IOP ∧ w ∈ IOC ∪ IDC | <y,x> ∈ EXTI(SI(owl:onProperty)) ∧ <y,w> ∈ EXTI(SI(owl:someValuesFrom)) |
| x ∈ IOP ∧ w ∈ IOT ∪ LV | <y,x> ∈ EXTI(SI(owl:onProperty)) ∧ <y,w> ∈ EXTI(SI(owl:hasValue)) |
| x ∈ IOP ∧ w ∈ LV ∧ w is a non-negative integer | <y,x> ∈ EXTI(SI(owl:onProperty)) ∧ <y,w> ∈ EXTI(SI(owl:minCardinality)) |
| x ∈ IOP ∧ w ∈ LV ∧ w is a non-negative integer | <y,x> ∈ EXTI(SI(owl:onProperty)) ∧ <y,w> ∈ EXTI(SI(owl:maxCardinality)) |
| x ∈ IOP ∧ w ∈ LV ∧ w is a non-negative integer | <y,x> ∈ EXTI(SI(owl:onProperty)) ∧ <y,w> ∈ EXTI(SI(owl:cardinality)) |
OWL Lite follows the following rules for OWL/DL.
OWL/DL augments the above conditions with a separation of the domain of discourse into several disjoint parts. This separation has two consequences. First, the OWL portion of the domain of discourse becomes standard first-order, in that predicates (classes and properties) and objects are disjoint. Second, the OWL portion of a OWL/DL interpretation can be viewed as a Description Logic interpretation for a particular expressive Description Logic.
A OWL/DL interpretation over a vocabulary V', where V' includes VRDFS, rdfs:Literal, VOWL, owl:Thing, and owl:Nothing, is an OWL interpretation as above that satisfies the following conditions.
The domain of discourse is divided up into several pieces.
| LV, IOT, IOC, IDC, IOP, and IL are all pairwise disjoint. |
| There is a disjoint partition of IOP into IOOP and IODP. |
| For n ∈ VRDFS∪VOWL - {rdf:nil}, SI(n) ∈ RI - (LV∪IOT∪IOC∪IDC∪IOP∪IL). |
Now entailment in OWL/DL can be defined.
Let K be an RDF graph and let V be a vocabulary that includes VRDFS, rdfs:Literal, VOWL, owl:Thing, and owl:Nothing. An OWL/DL interpretation of K is an OWL/DL interpretation over V that is also an RDFS interpretation of K.
Is imports part of OWL Lite?
Let K be a set of n-triples. The imports closure of K is the smallest superset of K such that if the imports closure of K contains a triple of the form x owl:imports y . where x is the empty URI and y is any URI then the imports closure of K contains the n-triples resulting from the RDF parsing of the document, if any, accessible at y into n-triples.
Let K and Q be collections of n-triples and let V be a vocabulary that includes VRDFS, rdfs:Literal, VOWL, owl:Thing, and owl:Nothing. Then K OWL/DL entails Q whenever all OWL/DL interpretations of the RDF graph specified by imports closure of K are also OWL/DL interpretations of the RDF graph specified by imports closure of Q.