- From: Ian Horrocks <horrocks@cs.man.ac.uk>
- Date: Mon, 9 Dec 2002 10:46:02 +0000
- To: "Jeremy Carroll" <jjc@hplb.hpl.hp.com>
- Cc: <www-webont-wg@w3.org>
On December 6, Jeremy Carroll writes:
>
> In the current semantics draft, OWL Lite just gets the same semantics as OWL
> DL on the syntactic subset.
> It would be possible in our one-dimensional layering to give OWL Lite a
> reduced semantics.
The current design ensures that, in principal, all language layers
give the same meaning to ontologies within their given syntactic
subset. I.e., given two ontologies O1 and O2 in the OWL Lite subset,
O1 OWL Lite entails O2 iff O1 OWL DL entails O2 iff O1 OWL full
entails O2; similarly, for O3, O4 in the OWL DL subset, O3 OWL DL
entails O4 iff O3 OWL full entails O4.
This seems to be a highly desirable property - we certainly spent
enough time trying to get it right at the interface between OWL DL and
OWL full - and I am at a loss to see why we should now consider
casually discarding it. As both Peter and Pat already pointed out,
there is no concrete evidence that the new semantics would confer any
benefit from a computational perspective, and it would seriously
damage interoperability as different OWL reasoners could different
results w.r.t. the same ontologies, while all still claiming to be
fully compliant.
Finally, I think that it is rather ridiculous to appeal to the feature
synopsis as though it where a requirements analysis for entailment. I
know of many applications where OWL Lite would be adequate in terms of
expressive power, but where entailments relying on iff semantics for
owl:sameClassAs are essential.
Regards, Ian
>
> This has the following advantages:
> - clearly differentiation between the two
> - much easier to implement OWL Lite so it really becomes an entry level
>
> I attach a modified version of section 5 of the semantics doc that changes a
> few iffs to if-then's, and drops comprehension.
>
> As far as I can tell, teh vast majority of the entailments discussed in the
> feature synopsis under OWL Lite are preserved, at much easier
> implementability.
>
> Also we can add hasValue without any difficulty.
>
> It permits a conformance statement, in a subsequent e-mail, that has no
> leeway, but is truely Lite.
>
> Jeremy
>
>
>
>
>
> <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
> "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
> <html lang="en-US" xml:lang="en-US" xmlns="http://www.w3.org/1999/xhtml">
>
> <head>
>
> <meta http-equiv="Content-Type" content="text/html; charset=ISO-8859-1" />
> <title>Web Ontology Language (OWL) Lite semantics</title>
>
> <style type="text/css">
> /*<![CDATA[*/
> .added {
> BACKGROUND: white; COLOR: green; TEXT-DECORATION: underline
> }
> .removed {
> BACKGROUND: white; COLOR: red; TEXT-DECORATION: line-through
> }
>
> /*]]>*/
> </style>
> <link rel="stylesheet" type="text/css" href="./spec.css" />
> <link rel="stylesheet" type="text/css"
> href="http://www.w3.org/StyleSheets/TR/base"/>
>
> </head>
>
> <body>
>
> <div class="navbar">
> <a href="mapping.html">previous</a>
> <a href="proofs.html">next</a>
> <a href="./">top</a>
> <a href="./#contents">contents</a>
> <hr />
> </div>
> <p>Last Modified by Carroll based on the published WD</p>
> <h2><a name="5"></a>OWL-Lite Semantics based on 5. RDFS-Compatible Model-Theoretic Semantics </h2>
>
>
> <p>
> Using
> this model-theoretic semantics for OWL Lite
> defines owl-lite-entailment, such whenever <i>A</i> owl-lite-entails <i>B</i>
> then <i>A</i> owl-entails <i>B</i> (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.
> </p>
>
> <p>OWL Lite is a subset of OWL DL, and the semantics is
> a minor modification of the OWL DL semantics.
> The goals are:
> </p>
> <ul>
> <li>To permit simple A-Box reasoning</li>
> <li>To have an easy entry level for both implementors and users</li>
> </ul>
> <p>
> 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.
> </p>
> <h3><a name="5.2"></a>5.2. OWL<span class="added"> Lite</span> Interpretations</h3>
> <span class="added">Change control from here on</span>
> <p>
> >From the RDF model theory
> [<cite><a href="./#ref-rdfmt">RDF MT</a></cite>],
> for V a set of URI references containing the RDF and RDFS vocabulary,
> an RDFS interpretation over V is a triple
> I = < R<sub>I</sub>, EXT<sub>I</sub>, S<sub>I</sub> >.
> Here R<sub>I</sub> is the domain of discourse or universe, i.e., a set that
> contains the denotations of URI references.
> EXT<sub>I</sub> is used to give meaning to properties, and is
> a mapping from R<sub>I</sub> to sets of pairs over
> R<sub>I</sub> × (R<sub>I</sub>∪LV).
> Finally, S<sub>I</sub> is a mapping from V to R<sub>I</sub>
> that takes a URI reference to its denotation.
> CEXT<sub>I</sub> is then defined as
> CEXT<sub>I</sub>(c) =
> { x∈R<sub>I</sub> |
> <x,c>∈EXT<sub>I</sub>(S<sub>I</sub>(rdf:type)) }.
> RDFS interpretations must meet several conditions, as detailed in the RDFS
> model theory.
> For example, S<sub>I</sub>(rdfs:subClassOf) must be a transitive
> relation.
> </p>
>
> <p>
> An OWL interpretation,
> I = < R<sub>I</sub>, EXT<sub>I</sub>, S<sub>I</sub> >,
> 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:
> </p>
>
> <p><strong>Relationships between OWL classes</strong></p>
>
> <table border="1">
> <thead>
> <tr> <th>If E is</th> <th>then
> CEXT<sub>I</sub>(S<sub>I</sub>(E))=</th> <th>with</th> </tr>
> </thead>
> <tbody>
> <tr> <td>owl:Thing</td> <td>IOT</td><td>IOT⊆R<sub>I</sub></td> </tr>
> <tr> <td>owl:Nothing</td> <td>{}</td><td></td> </tr>
> <tr> <td>rdfs:Literal</td> <td>LV</td><td></td> </tr>
> <tr> <td>owl:Class</td> <td>IOC</td><td>IOC⊆CEXT<sub>I</sub>(S<sub>I</sub>(rdfs:Class))</td> </tr>
> <tr> <td>owl:Restriction</td> <td>IOR</td><td>IOR⊆IOC</td> </tr>
> <tr> <td>owl:Datatype</td> <td>IDC</td><td>IDC⊆CEXT<sub>I</sub>(S<sub>I</sub>(rdfs:Class))</td> </tr>
> <tr> <td>owl:Property</td> <td>IOP</td><td>IOP⊆CEXT<sub>I</sub>(S<sub>I</sub>(rdf:Property))</td> </tr>
> <tr> <td>owl:ObjectProperty</td> <td>IOOP</td><td>IOOP⊆IOP</td> </tr>
> <tr> <td>owl:DataTypeProperty</td> <td>IODP</td><td>IODP⊆IOP </td> </tr>
> <tr> <td>rdf:List</td> <td>IL</td><td>IL⊆R<sub>I</sub> </td> </tr>
> </tbody>
> </table>
>
> <p><strong>Membership in OWL classes</strong></p>
>
> <table border="1">
> <thead>
> <tr><th>If E is </th><th>then S<sub>I</sub>(E)∈</th></tr>
> </thead>
> <tbody>
> <tr><td>owl:Thing</td><td>IOC</td></tr>
> <tr><td>owl:Nothing</td><td>IOC</td></tr>
> <tr><td>rdfs:Literal</td><td>IDC</td></tr>
> <tr><td>a datatype of D</td><td>IDC</td></tr>
> <tr><td>rdf:nil</td><td>IL</td></tr>
> </tbody>
> </table>
>
> <p><strong>Characteristics of members of OWL classes</strong></p>
>
> <table border="1">
> <thead>
> <tr><th>If E is </th><th>then if e∈CEXT<sub>I</sub>(S<sub>I</sub>(E)) then </th> </tr>
> </thead>
> <tbody>
> <tr><td>owl:Class</td><td>CEXT<sub>I</sub>(e)⊆IOT</td></tr>
> <tr><td>owl:Datatype</td><td>CEXT<sub>I</sub>(e)⊆LV</td></tr>
> <tr><td>owl:ObjectProperty</td><td>EXT<sub>I</sub>(e)⊆IOT×IOT</td></tr>
> <tr><td>owl:DatatypeProperty</td><td>EXT<sub>I</sub>(e)⊆IOT×LV</td></tr>
> </tbody>
> </table>
>
> <p>
> The next constraints are <span class="removed">IFF</span><span class="added">If-Then</span>,
> <span class="removed">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. </span>
> </p>
>
> <table border="1">
> <thead>
> <tr><th>If E is </th><th>then <span class="added">if</span> c∈CEXT<sub>I</sub>(S<sub>I</sub>(E))
> <span class="removed">iff </span> <span class="added">then</span> c∈IOP and </th> </tr>
> </thead>
> <tbody>
> <tr> <td>owl:SymmetricProperty</td>
> <td><x,y> ∈ EXT<sub>I</sub>(c)
> → <y, x>∈EXT<sub>I</sub>(c)</td> </tr>
> <tr> <td>owl:FunctionalProperty</td>
> <td><x,y<sub>1</sub>> and <x,y<sub>2</sub>>
> ∈ EXT<sub>I</sub>(c)
> → y<sub>1</sub> = y<sub>2</sub></td> </tr>
> <tr> <td>owl:InverseFunctionalProperty</td>
> <td><x<sub>1</sub>,y>∈EXT<sub>I</sub>(c)
> ∧ <x<sub>2</sub>,y>∈EXT<sub>I</sub>(c)
> → x<sub>1</sub> = x<sub>2</sub></td> </tr>
> <tr> <td>owl:TransitiveProperty</td>
> <td> <x,y>∈EXT<sub>I</sub>(c)
> ∧ <y,z>∈EXT<sub>I</sub>(c)
> → <x,z>∈EXT<sub>I</sub>(c)</td> </tr>
> </tbody>
> </table>
> <span class="removed">
> <p><strong>RDFS domains and ranges are strengthened
> to if-and-only-if over the OWL universe. </strong></p>
> </span>
> <p><strong>Some OWL properties have <span class="removed">iff</span><span class="added">if-then</span> characterizations</strong></p>
>
> <table border="1">
>
> <thead>
> <tr> <th>If E is</th>
> <th>then <span class="added">if</span> <x,y>∈EXT<sub>I</sub>(S<sub>I</sub>(E))
> <span class="removed">iff</span><span class="added">then</span></th> </tr>
> </thead>
> <tbody>
> <tr> <td>owl:sameClassAs</td>
> <td>x,y∈IOC ∧ CEXT<sub>I</sub>(x)=CEXT<sub>I</sub>(y)</td> </tr>
> <tr> <td>owl:disjointWith</td>
> <td>x,y∈IOC ∧ CEXT<sub>I</sub>(x)∩CEXT<sub>I</sub>(y)={}</td> </tr>
> <tr> <td>owl:samePropertyAs</td>
> <td>x,y∈IOP ∧ EXT<sub>I</sub>(x) = EXT<sub>I</sub>(y)</td> </tr>
> <tr> <td>owl:inverseOf</td>
> <td>x,y∈IOOP ∧ <u,v>∈EXT<sub>I</sub>(x) iff
> <v,u>∈EXT<sub>I</sub>(y)</td>
> </tr>
> <tr> <td>owl:sameIndividualAs</td> <td>x = y </td> </tr>
> <tr> <td>owl:sameAs</td> <td>x = y </td> </tr>
> <tr> <td>owl:differentFrom</td> <td>x ≠ y </td> </tr>
> </tbody>
> </table>
>
> <p><strong>Some OWL properties have only-if characterizations</strong></p>
>
> <p>
> We will say that l<sub>1</sub> is a sequence of
> y<sub>1</sub>,…,y<sub>n</sub> over C iff
> n=0 and l<sub>1</sub>=S<sub>I</sub>(rdf:nil)
> or n>0 and l<sub>1</sub>∈IL and
> ∃ l<sub>2</sub>, …, l<sub>n</sub> ∈ IL such that
> <br />
> <l<sub>1</sub>,y<sub>1</sub>>∈EXT<sub>I</sub>(S<sub>I</sub>(rdf:first)), y<sub>1</sub>∈CEXT<sub>I</sub>(C),
> <l<sub>1</sub>,l<sub>2</sub>>∈EXT<sub>I</sub>(S<sub>I</sub>(rdf:rest)), …, <br />
> <l<sub>n</sub>,y<sub>n</sub>>∈EXT<sub>I</sub>(S<sub>I</sub>(rdf:first)), y<sub>n</sub>∈CEXT<sub>I</sub>(C), and
> <l<sub>n</sub>,S<sub>I</sub>(rdf:nil)>∈EXT<sub>I</sub>(S<sub>I</sub>(rdf:rest)).
> </p>
>
> <table border="1">
>
> <thead>
> <tr> <th>If E is</th>
> <th>then if <x,y>∈EXT<sub>I</sub>(S<sub>I</sub>(E)) then</th>
> </tr>
> </thead>
> <tbody>
> <tr> <td class="removed">owl:complementOf</td>
> <td class="removed">x,y∈ IOC and CEXT<sub>I</sub>(x)=IOT-CEXT<sub>I</sub>(y)</td>
> </tr>
> </tbody>
> </table>
>
> <table border="1">
> <thead>
> <tr> <th>If E is</th>
> <th>then if <x,l>∈EXT<sub>I</sub>(S<sub>I</sub>(E)) then</th>
> </tr>
> </thead>
> <tbody>
> <tr> <td class="removed">owl:unionOf</td>
> <td class="removed">x∈IOC and l is a sequence of
> y<sub>1</sub>,…y<sub>n</sub> over IOC and
> CEXT<sub>I</sub>(x) =
> CEXT<sub>I</sub>(y<sub>1</sub>)∪…∪CEXT<sub>I</sub>(y<sub>n</sub>)</td>
> </tr>
> <tr> <td>owl:intersectionOf</td>
> <td>x∈IOC and l is a sequence of
> y<sub>1</sub>,…y<sub>n</sub> over IOC and
> CEXT<sub>I</sub>(x) = CEXT<sub>I</sub>(y<sub>1</sub>)∩…∩CEXT<sub>I</sub>(y<sub>n</sub>)</td>
> </tr>
> <tr> <td>owl:oneOf</td>
> <td>x∈CEXT<sub>I</sub>(rdfs:Class) and l is a sequence of
> y<sub>1</sub>,…y<sub>n</sub> over R<sub>I</sub>∪LV and
> CEXT<sub>I</sub>(x) = {y<sub>1</sub>,..., y<sub>n</sub>}
> </td> </tr>
> </tbody>
> </table>
>
> <table border="1">
> <thead>
> <tr> <th>If E is</th><th>and</th>
> <th>then if <x,l>∈EXT<sub>I</sub>(S<sub>I</sub>(E)) then</th> </tr>
> </thead>
> <tbody>
> <tr> <td>owl:oneOf</td><td>l is a sequence of y<sub>1</sub>,…y<sub>n</sub> over LV</td>
> <td>x∈IDC and CEXT<sub>I</sub>(x) = {y<sub>1</sub>,..., y<sub>n</sub>} </td> </tr>
> <tr> <td>owl:oneOf</td><td>l is a sequence of y<sub>1</sub>,…y<sub>n</sub> over IOT</td>
> <td>x∈IOC and CEXT<sub>I</sub>(x) = {y<sub>1</sub>,..., y<sub>n</sub>} </td> </tr>
> </tbody>
> </table>
>
> <p class="added">Todo: think about oneof</p>
> <table border="1">
>
>
> <tr> <th>If</th>
> <th>then x∈IOR, y∈IOC, p∈IOP, and CEXT<sub>I</sub>(x) =</th>
> </tr>
>
> <tr> <td><x,y>∈EXT<sub>I</sub>(S<sub>I</sub>(owl:allValuesFrom))) ∧ <br />
> <x,p>∈EXT<sub>I</sub>(S<sub>I</sub>(owl:onProperty)))</td>
> <td>{u∈IOT | <u,v>∈EXT<sub>I</sub>(p) → v∈CEXT<sub>I</sub>(y) }</td>
> </tr>
> <tr> <td><x,y>∈EXT<sub>I</sub>(S<sub>I</sub>(owl:someValuesFrom))) ∧ <br />
> <x,p>∈EXT<sub>I</sub>(S<sub>I</sub>(owl:onProperty)))</td>
> <td>{u∈IOT | ∃ <u,v>∈EXT<sub>I</sub>(p)
> ∧ v∈CEXT<sub>I</sub>(y) } </td>
> </tr>
> <tr> <td><x,y>∈EXT<sub>I</sub>(S<sub>I</sub>(owl:hasValue))) ∧ <br />
> <x,p>∈EXT<sub>I</sub>(S<sub>I</sub>(owl:onProperty)))</td>
> <td>{u∈IOT | <u, y>∈EXT<sub>I</sub>(p) }</td>
> </tr>
>
>
> <tr> <th>If</th>
> <th>then x∈IOR, y∈LV, y is a non-negative integer, p∈IOP, and CEXT<sub>I</sub>(x) =</th>
> </tr>
> <tr> <td><x,y>∈EXT<sub>I</sub>(S<sub>I</sub>(owl:minCardinality))) ∧ <br />
> <x,p>∈EXT<sub>I</sub>(S<sub>I</sub>(owl:onProperty)))</td>
> <td>{u∈IOT | card({v : <u,v>∈EXT<sub>I</sub>(p)}) ≥ y }</td>
> </tr>
> <tr> <td><x,y>∈EXT<sub>I</sub>(S<sub>I</sub>(owl:maxCardinality))) ∧ <br />
> <x,p>∈EXT<sub>I</sub>(S<sub>I</sub>(owl:onProperty)))</td>
> <td>{u∈IOT | card({v : <u,v>∈EXT<sub>I</sub>(p)}) ≤ y }</td>
> </tr>
> <tr> <td><x,y>∈EXT<sub>I</sub>(S<sub>I</sub>(owl:cardinality))) ∧ <br />
> <x,p>∈EXT<sub>I</sub>(S<sub>I</sub>(owl:onProperty)))</td>
> <td>{u∈IOT | card({v : <u,v>∈EXT<sub>I</sub>(p)}) = y }</td>
> </tr>
>
> </table>
>
> <p class="removed"><strong>R<sub>I</sub> contains elements corresponding to all possible OWL
> descriptions and data ranges</strong></p>
>
> <p class="added">Maybe the comprehension principle on lists should go too.
> Leaving it in for now.</p>
> <p>
> 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.
> </p>
>
> <table border="1">
>
> <thead>
> <tr><th>If there exists</th>
> <th>then there exists l<sub>1</sub>,…,l<sub>n</sub> ∈ IL with</th></tr>
> </thead>
> <tbody>
> <tr><td>x<sub>1</sub>, …, x<sub>n</sub> ∈ IOC</td>
> <td><l<sub>1</sub>,x<sub>1</sub>> ∈ EXT<sub>I</sub>(S<sub>I</sub>(rdf:first)),
> <l<sub>1</sub>,l<sub>2</sub>> ∈ EXT<sub>I</sub>(S<sub>I</sub>(rdf:rest)), … <br />
> <l<sub>n</sub>,x<sub>n</sub>> ∈ EXT<sub>I</sub>(S<sub>I</sub>(rdf:first)),
> <l<sub>n</sub>,S<sub>I</sub>(rdf:nil)> ∈ EXT<sub>I</sub>(S<sub>I</sub>(rdf:rest))</td></tr>
> <tr><td>x<sub>1</sub>, …, x<sub>n</sub> ∈ IOT∪LV</td>
> <td><l<sub>1</sub>,x<sub>1</sub>> ∈ EXT<sub>I</sub>(S<sub>I</sub>(rdf:first)),
> <l<sub>1</sub>,l<sub>2</sub>> ∈ EXT<sub>I</sub>(S<sub>I</sub>(rdf:rest)), … <br />
> <l<sub>n</sub>,x<sub>n</sub>> ∈ EXT<sub>I</sub>(S<sub>I</sub>(rdf:first)),
> <l<sub>n</sub>,S<sub>I</sub>(rdf:nil)> ∈ EXT<sub>I</sub>(S<sub>I</sub>(rdf:rest))</td></tr>
> </tbody>
> </table><p class="added">All of the following comprehension principls go,
> except possibly that for intersection, my preference is for it to go, too.</p>
> <div class="removed">
> <table border="1">
>
>
>
> <tr class="removed"><th class="removed">If there exists</th>
> <th class="removed">then there exists y with</th></tr>
>
>
> <tr class="removed"><td class="removed">l, a sequence of x<sub class="removed" 1</sub>,…,x<sub class="removed">n</sub> over IOC</td>
> <td class="removed">y∈IOC, <y,l> ∈ EXT<sub class="removed">I</sub>(S<sub class="removed">I</sub>(owl:unionOf))</td></tr>
> <tr class="removed"><td class="removed">l, a sequence of x<sub class="removed">1</sub>,…,x<sub class="removed">n</sub> over IOC</td>
> <td class="removed">y∈IOC, <y,l> ∈ EXT<sub class="removed">I</sub>(S<sub class="removed">I</sub>(owl:intersectionOf))</td></tr>
> <tr class="removed"><td class="removed">l, a sequence of x<sub class="removed">1</sub>,…,x<sub class="removed">n</sub> over IOT∪LV</td>
> <td class="removed">y∈CEXT<sub class="removed">I</sub>(S<sub class="removed">I</sub>(rdfs:Class)),
> <y,l> ∈ EXT<sub class="removed">I</sub>(S<sub class="removed">I</sub>(owl:oneOf))</td></tr>
>
>
>
> <tr class="removed"><th class="removed">If there exists</th>
> <th class="removed">then there exists y ∈ IOC with</th></tr>
>
>
> <tr class="removed"><td class="removed">x ∈ IOC</td>
> <td class="removed"><y,x> ∈ EXT<sub class="removed">I</sub>(S<sub class="removed">I</sub>(owl:complementOf))</td></tr>
>
>
>
> <tr class="removed"><th class="removed">If there exists</th>
> <th class="removed">then there exists y ∈ IOR with</th></tr>
>
>
> <tr class="removed"><td class="removed">x ∈ IOP ∧
> w ∈ IOC ∪ IDC</td>
> <td class="removed"><y,x> ∈ EXT<sub class="removed">I</sub>(S<sub class="removed">I</sub>(owl:onProperty)) ∧<br />
> <y,w> ∈ EXT<sub class="removed">I</sub>(S<sub class="removed">I</sub>(owl:allValuesFrom))</td></tr>
> <tr class="removed"><td class="removed">x ∈ IOP ∧
> w ∈ IOC ∪ IDC</td>
> <td class="removed"><y,x> ∈ EXT<sub class="removed">I</sub>(S<sub class="removed">I</sub>(owl:onProperty)) ∧<br />
> <y,w> ∈ EXT<sub class="removed">I</sub>(S<sub class="removed">I</sub>(owl:someValuesFrom))</td></tr>
> <tr class="removed"><td class="removed">x ∈ IOP ∧
> w ∈ IOT ∪ LV</td>
> <td class="removed"><y,x> ∈ EXT<sub class="removed">I</sub>(S<sub class="removed">I</sub>(owl:onProperty)) ∧<br />
> <y,w> ∈ EXT<sub>I</sub>(S<sub>I</sub>(owl:hasValue))</td></tr>
> <tr class="removed"><td class="removed">x ∈ IOP ∧
> w ∈ LV ∧ w is a non-negative integer</td>
> <td class="removed"><y,x> ∈ EXT<sub class="removed">I</sub>(S<sub class="removed">I</sub>(owl:onProperty)) ∧<br />
> <y,w> ∈ EXT<sub class="removed">I</sub>(S<sub class="removed">I</sub>(owl:minCardinality))</td></tr>
> <tr class="removed"><td class="removed">x ∈ IOP ∧
> w ∈ LV ∧ w is a non-negative integer</td>
> <td class="removed"><y,x> ∈ EXT<sub class="removed">I</sub>(S<sub class="removed">I</sub>(owl:onProperty)) ∧<br />
> <y,w> ∈ EXT<sub class="removed">I</sub>(S<sub class="removed">I</sub>(owl:maxCardinality))</td></tr>
> <tr class="removed"><td class="removed">x ∈ IOP ∧
> w ∈ LV ∧ w is a non-negative integer</td>
> <td class="removed"><y,x> ∈ EXT<sub class="removed">I</sub>(S<sub class="removed">I</sub>(owl:onProperty)) ∧<br />
> <y,w> ∈ EXT<sub class="removed">I</sub>(S<sub class="removed">I</sub>(owl:cardinality))</td></tr>
>
>
> </table>
>
> </div>
> <h3><a name="5.3"></a>5.3. OWL/DL</h3>
>
> <p class="added">OWL Lite follows the following rules for OWL/DL.
> </p>
> <p>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.
> </p>
>
> <p>
> 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.
> </p>
>
>
> <p><strong>The domain of discourse is divided up into several pieces. </strong></p>
>
> <table border="1">
> <tr><td> LV, IOT, IOC, IDC, IOP, and IL are all pairwise disjoint. </td></tr>
> <tr><td> There is a disjoint partition of IOP into IOOP and IODP. </td></tr>
> <tr><td> For n ∈ VRDFS∪VOWL - {rdf:nil},
> S<sub>I</sub>(n) ∈ R<sub>I</sub> - (LV∪IOT∪IOC∪IDC∪IOP∪IL). </td></tr>
> </table>
>
>
> <h4><a name="5.3.1"></a>5.3.1. OWL/DL Entailment</h4>
>
> <p>
> Now entailment in OWL/DL can be defined.
> </p>
>
> <p>
> Let K be an RDF graph
> and let V be a vocabulary that includes
> VRDFS, rdfs:Literal, VOWL, owl:Thing, and owl:Nothing.
> An <em>OWL/DL interpretation of K</em>
> is an OWL/DL interpretation over V
> that is also an RDFS interpretation of K.
> </p>
> <p class ="added">Is imports part of OWL Lite?</p>
> <p>
> Let K be a set of n-triples.
> The <em>imports closure</em> 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.
> </p>
>
> <p>
> 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 <em>K OWL/DL entails Q</em>
> 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.
> </p>
> <hr />
>
> </body>
> </html>
>
Received on Monday, 9 December 2002 05:46:31 UTC