From: <connolly@jammer.dm93.org>

Date: Wed, 29 May 2002 18:56:34 -1000

To: www-webont-wg@w3.org

Message-Id: <E17DHzG-0005pC-00@jammer.dm93.org>

Date: Wed, 29 May 2002 18:56:34 -1000

To: www-webont-wg@w3.org

Message-Id: <E17DHzG-0005pC-00@jammer.dm93.org>

Jeremy wrote: >> I think there are two proposals that I think we can be confident would >> work: one in which all the ontology stuff is dark, and one in which no >> sets necessarily exist. Then peter wrote: >The first definitely works. There is not yet an existence proof that the >second does indeed work, at least as an extension of the RDF model theory. [...] > If you mean a same-syntax >extension, then, again, that is impossible for the uppper layers without > going to a very non-standard logic. -- http://lists.w3.org/Archives/Public/www-webont-wg/2002May/0236.html So tonight I started writing up a model theory. I worked out the details for about 10 of the 30 or so terms in DAML+OIL; I'm pretty sure the rest are straightforward, but it's getting tedious and I'm getting tired, so I'm taking a break for the night... Jeremy, wanna look this over and maybe fill in the next few terms? ========== As in [RDFMT], an interpretation I of a vocabulary V is 1. A non-empty set IR of resources, called the domain or universe of I. 2. A mapping IEXT from IR into the powerset of IR x (IR union LV) i.e. the set of sets of pairs <x,y> with x in IR and y in IR or LV 3. A mapping IS from V into IR Every owl interpretations is an RDF interpretations (i.e. IR contains IS(rdf:type)) and an RDFS interpretation (i.e. the RDFS closure rules apply). Recall that ICEXT(x) abbreviates {y | <y,x> is in IEXT(I(rdf:type)) }. Likewise, let ICEXT(x) abbreviates {y | <y,x> is in IEXT(I(rdf:type)) }. Additionally, owl reserves the following vocabulary: * cardinality * complementOf * differentIndividualFrom * disjointUnionOf * disjointWith * equivalentTo * hasClass * hasValue * imports * intersectionOf * inverseOf * maxCardinality * minCardinality * oneOf * onProperty * Ontology * Restriction * sameClassAs * sameIndividualAs * samePropertyAs * subClassOf * subPropertyOf * toClass * TransitiveProperty * UnambigousProperty * unionOf * UniqueProperty * versionInfo * first * rest * nil * item * List That is, it reserves the URI references http://www.w3.org/2001/10/daml+oil#cardinality , http://www.w3.org/2001/10/daml+oil#complementOf , and so on; in this document, we'll abbreviate these as ont:cardinality, ont:complementOf and so on. The following closure rules apply: ?l ont:first ?x. ==> ?l ont:item ?x. ?l ont:rest ?r. ?r ont:first ?x. ==> ?l ont:item ?x. The following constraints on interpretations apply: cardinality: if ?nl is a numeral for ?n (i.e. ?nl is a string that is a lexical representation of the integer ?n), and <IS(?p), ?nl> is in IEXT(I(ont:cardinality)) and <?s, ?o> is in IEXT(?p), then the size of the set { ?x: <?s, ?x> is in IEXT(?p) } is ?n. complementOf: if <?s, ?o> is in IEXT(I(ont:complementOf)), then ICEXT(?s) is the complement of ICEXT(?o) relative to IR. differentIndividualFrom: if <?s, ?o> is in IEXT(I(ont:differentIndividualFrom)), then ?s is not equal to ?o. disjointUnionOf: 1. if <?s, ?l> is in IEXT(I(ont:disjointUnionOf)), and <?l, ?a> is in IEXT(I(ont:item)), then ICEXT(?a) is a subset of ICEXT(?s). 2. if <?s, ?l> is in IEXT(I(ont:disjointUnionOf)), and <?l, ?a> is in IEXT(I(ont:first)), and <?l, ?r> is in IEXT(I(ont:rest)), and <?x, ?s> is in IEXT(I(rdf:type)), then either ?x is in ICEXT(?a) or there is a ?b where <?r, ?b> is in IEXT(I(ont:item)). 3. if <?s, ?l> is in IEXT(I(ont:disjointUnionOf)), then ?l is a pairwise-disjoint list, defined recursively as follows: IEXT(I(ont:nil)) is pairwise-disjoint. any ?l with <?l, IS(ont:nil)> in IEXT(I(ont:rest)) is pairwise-disjoint. if ?r is pairwise-disjoint, and <?l, ?a> in IEXT(I(ont:first)), and for each ?b with <?r, ?b> in IEXT(I(ont:item)), ICEXT(?a) is disjoint with ICEXT(?b), then ?l is pairwise-disjoint. disjointWith: if <?s, ?o> is in IEXT(I(ont:disjointWith)), then ICEXT(?s) is disjoint from ICEXT(?o). equivalentTo: if <?s, ?o> is in IEXT(I(ont:equivalentTo)), then IEXT(?s) = IEXT(?o). onProperty/hasClass: if <?r, ?p> is in IEXT(I(ont:onProperty)) and <?r, ?a> is in IEXT(I(ont:hasClass)), then the set { ?o: for some ?s in ICEXT(?r), <?s, ?o> is in IEXT(?p) and ?o is in ICEXT(?a) } isn't empty. onProperty/hasValue: if <?r, ?p> is in IEXT(I(ont:onProperty)) and <?r, ?a> is in IEXT(I(ont:hasValue)), then the set { ?o: for some ?s in ICEXT(?r), <?s, ?a> is in IEXT(?p) } isn't empty. [... and so on...] Notes: dropped per WG decision: * cardinalityQ * hasClassQ * maxCardinalityQ * minCardinalityQ dropped re 'uniform treatment of literals' * Datatype * DatatypeProperty * DatatypeRestriction * ObjectClass * ObjectProperty * ObjectRestriction already specified by RDF MT: * domain * Property * range * Class [RDFMT] RDF Model Theory W3C Working Draft 29 April 2002 http://www.w3.org/TR/2002/WD-rdf-mt-20020429/ esp section http://www.w3.org/TR/2002/WD-rdf-mt-20020429/#sinterpReceived on Thursday, 30 May 2002 00:57:28 GMT

*
This archive was generated by hypermail 2.2.0+W3C-0.50
: Monday, 7 December 2009 10:57:50 GMT
*