RE: RDF and OWL rules

Hi Geoff,

> I'm struggling a bit with one of the test cases [1]. It makes intuitive
> sense to me but I can't quite see how it works according to the
> semantics doc [2]. I'm hoping you might be able to point out where I'm
> going wrong in my reasoning.
>
> In this test case, the premise is a cardinality restriction on a
> property. The conclusion is that the restriction in the premise is
> identical to an intersection of an equivalent min and max cardinality on
> the same property.
>
> I can see how the conclusion could say that the restriction C in the
> premise is an equivalentClass to some class that is an intersectionOf
> the two new restrictions (i.e. they have the same class extension), but
> I'm having trouble seeing what licenses one to say that they (the two
> classes) are one and the same.
>
> Perhaps there's something wrong with my understanding of the semantics
> of intersectionOf? My understanding is that they are if, not iff. I
> thought that meant that we can't infer that C is an intersection of A
> and B just because we know that the class extension of C is the same as
> the intersection of the class extensions of A and B. (this confuses me
> somewhat because I thought I'd received contradictory replies to a
> similar query on rdf logic[3] - but perhaps I was too imprecise in what
> I asked)

Right now I was trying owl:intersectionOf too
to get an answer for

:i a ?I.
?I owl:intersectionOf ?L1.
?L1 a rdf:List.
?L1 rdf:first :B.
?L1 rdf:rest ?L2.
?L2 a rdf:List.
?L2 rdf:first :C.
?L2 rdf:rest ?L3.
?L3 a rdf:List.
?L3 rdf:first :A.
?L3 rdf:rest rdf:nil

given that

:i rdf:type :A.
:i rdf:type :B.
:i rdf:type :C.

and we can resolve that as shown in [R1] assuming
following comprehension rules

{?X a ?U, ?V, ?W} => {?X a (?U ?V ?W).:sf1}.
{?X a ?U, ?V, ?W} => {(?U ?V ?W).:sf1 owl:intersectionOf (?U ?V ?W).:sf2}.
{?X a ?U, ?V, ?W} => {(?U ?V ?W).:sf2 a rdf:List}.
{?X a ?U, ?V, ?W} => {(?U ?V ?W).:sf2 rdf:first ?U}.
{?X a ?U, ?V, ?W} => {(?U ?V ?W).:sf2 rdf:rest (?U ?V ?W).:sf3}.
{?X a ?U, ?V, ?W} => {(?U ?V ?W).:sf3 a rdf:List}.
{?X a ?U, ?V, ?W} => {(?U ?V ?W).:sf3 rdf:first ?V}.
{?X a ?U, ?V, ?W} => {(?U ?V ?W).:sf3 rdf:rest (?U ?V ?W).:sf4}.
{?X a ?U, ?V, ?W} => {(?U ?V ?W).:sf4 a rdf:List}.
{?X a ?U, ?V, ?W} => {(?U ?V ?W).:sf4 rdf:first ?W}.
{?X a ?U, ?V, ?W} => {(?U ?V ?W).:sf4 rdf:rest rdf:nil}.

So I think that

{:i a [ owl:intersectionOf (:A :B :C)]} => {:i a :A, :B, :C}.
and
{:i a :A, :B, :C} => {:i a [ owl:intersectionOf (:A :B :C)]}.

but I'm not seeing how to do that for all cases...
Anyhow, I still think that [1] is OK at least we get [R2]


> I hope I've managed to explain myself :-)

I think so ;-)

> Regards,
>
> Geoff
>
> P.S. I think that rule4p1 is, strictly speaking, unnecessary since:
>
> owl:equivalentProperty rdfs:subPropertyOf rdfs:subPropertyOf; a
> owl:SymmetricProperty;
>
> (as long as the standard rdfs rules are included).

Strictly yes, but then without rule4p1 and the former rule4p2
(and in our implementation) we have trouble resolving
http://www.w3.org/2002/03owlt/mapVocabP =>
http://www.w3.org/2002/03owlt/mapVocabC

as well as
http://www.w3.org/2002/03owlt/equivalentProperty/Manifest001
and
http://www.w3.org/2002/03owlt/equivalentProperty/Manifest006

(which indeed is spotting an implementation weakness)


> [1] http://www.w3.org/2002/03owlt/cardinality/Manifest005
>
> [2]
> http://www.w3.org/TR/2003/WD-owl-semantics-20030331/rdfs.html#owl_AllDif
> ferent_rdf
>
> [3] http://lists.w3.org/Archives/Public/www-rdf-logic/2003Mar/0185.html

-- ,
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/

[R1]
@prefix str: <http://www.w3.org/2000/10/swap/string#> .
@prefix xsd: <http://www.w3.org/2001/XMLSchema#> .
@prefix : <file:/temp/test#> .
@prefix log: <http://www.w3.org/2000/10/swap/log#> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
@prefix math: <http://www.w3.org/2000/10/swap/math#> .
@prefix owl: <http://www.w3.org/2002/07/owl#> .
@prefix neg: <http://www.agfa.com/w3c/euler/owl-rules#> .
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .

 {{?X = :i. ?U = :B. ?X a ?U} log:implies {:i a :B} .
  {?X = :i. ?V = :C. ?X a ?V} log:implies {:i a :C} .
  {?X = :i. ?W = :A. ?X a ?W} log:implies {:i a :A} .
  ?I = (:B :C :A).:sf1. :i a ?I} log:implies
{:i a (:B :C :A).:sf1} .
 {{?X = :i. ?U = :B. ?X a ?U} log:implies {:i a :B} .
  {?X = :i. ?V = :C. ?X a ?V} log:implies {:i a :C} .
  {?X = :i. ?W = :A. ?X a ?W} log:implies {:i a :A} .
  ?I = (:B :C :A).:sf1. ?L1 = (:B :C :A).:sf2. ?I owl:intersectionOf ?L1}
log:implies
{(:B :C :A).:sf1 owl:intersectionOf (:B :C :A).:sf2} .
 {{?X = :i. ?U = :B. ?X a ?U} log:implies {:i a :B} .
  {?X = :i. ?V = :C. ?X a ?V} log:implies {:i a :C} .
  {?X = :i. ?W = :A. ?X a ?W} log:implies {:i a :A} .
  ?L1 = (:B :C :A).:sf2. ?L1 a rdf:List} log:implies
{(:B :C :A).:sf2 a rdf:List} .
 {{?X = :i. ?U = :B. ?X a ?U} log:implies {:i a :B} .
  {?X = :i. ?V = :C. ?X a ?V} log:implies {:i a :C} .
  {?X = :i. ?W = :A. ?X a ?W} log:implies {:i a :A} .
  ?L1 = (:B :C :A).:sf2. ?L1 rdf:first :B} log:implies
{(:B :C :A).:sf2 rdf:first :B} .
 {{?X = :i. ?U = :B. ?X a ?U} log:implies {:i a :B} .
  {?X = :i. ?V = :C. ?X a ?V} log:implies {:i a :C} .
  {?X = :i. ?W = :A. ?X a ?W} log:implies {:i a :A} .
  ?L1 = (:B :C :A).:sf2. ?L2 = (:B :C :A).:sf3. ?L1 rdf:rest ?L2}
log:implies
{(:B :C :A).:sf2 rdf:rest (:B :C :A).:sf3} .
 {{?X = :i. ?U = :B. ?X a ?U} log:implies {:i a :B} .
  {?X = :i. ?V = :C. ?X a ?V} log:implies {:i a :C} .
  {?X = :i. ?W = :A. ?X a ?W} log:implies {:i a :A} .
  ?L2 = (:B :C :A).:sf3. ?L2 a rdf:List} log:implies
{(:B :C :A).:sf3 a rdf:List} .
 {{?X = :i. ?U = :B. ?X a ?U} log:implies {:i a :B} .
  {?X = :i. ?V = :C. ?X a ?V} log:implies {:i a :C} .
  {?X = :i. ?W = :A. ?X a ?W} log:implies {:i a :A} .
  ?L2 = (:B :C :A).:sf3. ?L2 rdf:first :C} log:implies
{(:B :C :A).:sf3 rdf:first :C} .
 {{?X = :i. ?U = :B. ?X a ?U} log:implies {:i a :B} .
  {?X = :i. ?V = :C. ?X a ?V} log:implies {:i a :C} .
  {?X = :i. ?W = :A. ?X a ?W} log:implies {:i a :A} .
  ?L2 = (:B :C :A).:sf3. ?L3 = (:B :C :A).:sf4. ?L2 rdf:rest ?L3}
log:implies
{(:B :C :A).:sf3 rdf:rest (:B :C :A).:sf4} .
 {{?X = :i. ?U = :B. ?X a ?U} log:implies {:i a :B} .
  {?X = :i. ?V = :C. ?X a ?V} log:implies {:i a :C} .
  {?X = :i. ?W = :A. ?X a ?W} log:implies {:i a :A} .
  ?L3 = (:B :C :A).:sf4. ?L3 a rdf:List} log:implies
{(:B :C :A).:sf4 a rdf:List} .
 {{?X = :i. ?U = :B. ?X a ?U} log:implies {:i a :B} .
  {?X = :i. ?V = :C. ?X a ?V} log:implies {:i a :C} .
  {?X = :i. ?W = :A. ?X a ?W} log:implies {:i a :A} .
  ?L3 = (:B :C :A).:sf4. ?L3 rdf:first :A} log:implies
{(:B :C :A).:sf4 rdf:first :A} .
 {{?X = :i. ?U = :B. ?X a ?U} log:implies {:i a :B} .
  {?X = :i. ?V = :C. ?X a ?V} log:implies {:i a :C} .
  {?X = :i. ?W = :A. ?X a ?W} log:implies {:i a :A} .
  ?L3 = (:B :C :A).:sf4. ?L3 rdf:rest rdf:nil} log:implies
{(:B :C :A).:sf4 rdf:rest rdf:nil} .


[R2]
@prefix str: <http://www.w3.org/2000/10/swap/string#> .
@prefix ns: <http://www.agfa.com/w3c/euler/owl-rules#> .
@prefix xsd: <http://www.w3.org/2001/XMLSchema#> .
@prefix : <http://www.w3.org/2002/03owlt/cardinality/premises005#> .
@prefix daml: <http://www.daml.org/2001/03/daml+oil#> .
@prefix log: <http://www.w3.org/2000/10/swap/log#> .
@prefix nsnsnsns:
<http://www.w3.org/2002/03owlt/cardinality/conclusions005#> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
@prefix test: <http://www.w3.org/2000/10/rdf-tests/rdfcore/testSchema#> .
@prefix math: <http://www.w3.org/2000/10/swap/math#> .
@prefix nsns: <http://www.agfa.com/w3c/euler/xsd-rules#> .
@prefix owl: <http://www.w3.org/2002/07/owl#> .
@prefix nsnsns: <http://www.agfa.com/w3c/euler/rdfs-rules#> .
@prefix neg: <http://www.agfa.com/w3c/euler/negation#> .
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .

{?v3337447 = _:3083223_440.
<http://www.w3.org/2002/03owlt/cardinality/premises005#c>
<http://www.w3.org/2002/07/owl#intersectionOf> ?v3337447} log:implies
{<http://www.w3.org/2002/03owlt/cardinality/premises005#c>
<http://www.w3.org/2002/07/owl#intersectionOf> _:3083223_440} .
{?v3337447 = _:3083223_440. ?v3337447 a rdf:List} log:implies
{_:3083223_440 a rdf:List} .
{?v3337447 = _:3083223_440. ?v6254292 = _:3298944_440. ?v3337447 rdf:rest
?v6254292} log:implies {_:3083223_440 rdf:rest _:3298944_440} .
{?v6254292 = _:3298944_440. ?v6254292 a rdf:List} log:implies
{_:3298944_440 a rdf:List} .
{?v6254292 = _:3298944_440. ?v6254292 rdf:rest rdf:nil} log:implies
{_:3298944_440 rdf:rest rdf:nil} .
{?v6254292 = _:3298944_440. ?v6633755
= <http://www.w3.org/2002/03owlt/cardinality/premises005#c>. ?v6254292
rdf:first ?v6633755} log:implies {_:3298944_440 rdf:first
<http://www.w3.org/2002/03owlt/cardinality/premises005#c>} .
{?v6633755 = <http://www.w3.org/2002/03owlt/cardinality/premises005#c>.
?v6633755 a <http://www.w3.org/2002/07/owl#Restriction>} log:implies
{<http://www.w3.org/2002/03owlt/cardinality/premises005#c> a
<http://www.w3.org/2002/07/owl#Restriction>} .
 {
  <http://www.agfa.com/w3c/euler/owl-rules#rule10c3>.
  {?r = <http://www.w3.org/2002/03owlt/cardinality/premises005#c>. ?p
= <http://www.w3.org/2002/03owlt/cardinality/premises005#p>. ?r
owl:onProperty ?p} log:implies
{<http://www.w3.org/2002/03owlt/cardinality/premises005#c> owl:onProperty
<http://www.w3.org/2002/03owlt/cardinality/premises005#p>} .
  {?r = <http://www.w3.org/2002/03owlt/cardinality/premises005#c>. ?m = "1"
^^<http://www.w3.org/2001/XMLSchema#nonNegativeInteger>. ?r owl:cardinality
?m} log:implies {<http://www.w3.org/2002/03owlt/cardinality/premises005#c>
owl:cardinality "1"^^<http://www.w3.org/2001/XMLSchema#nonNegativeInteger>}
.
  ?v6633755 = <http://www.w3.org/2002/03owlt/cardinality/premises005#c>.
?v6633755 <http://www.w3.org/2002/07/owl#minCardinality> "1"
^^<http://www.w3.org/2001/XMLSchema#nonNegativeInteger>} log:implies
{<http://www.w3.org/2002/03owlt/cardinality/premises005#c>
<http://www.w3.org/2002/07/owl#minCardinality> "1"
^^<http://www.w3.org/2001/XMLSchema#nonNegativeInteger>} .
{?v6633755 = <http://www.w3.org/2002/03owlt/cardinality/premises005#c>.
?v6633755 <http://www.w3.org/2002/07/owl#onProperty>
<http://www.w3.org/2002/03owlt/cardinality/premises005#p>} log:implies
{<http://www.w3.org/2002/03owlt/cardinality/premises005#c>
<http://www.w3.org/2002/07/owl#onProperty>
<http://www.w3.org/2002/03owlt/cardinality/premises005#p>} .
{?v3337447 = _:3083223_440. ?v540994
= <http://www.w3.org/2002/03owlt/cardinality/premises005#c>. ?v3337447
rdf:first ?v540994} log:implies {_:3083223_440 rdf:first
<http://www.w3.org/2002/03owlt/cardinality/premises005#c>} .
{?v540994 = <http://www.w3.org/2002/03owlt/cardinality/premises005#c>.
?v540994 a <http://www.w3.org/2002/07/owl#Restriction>} log:implies
{<http://www.w3.org/2002/03owlt/cardinality/premises005#c> a
<http://www.w3.org/2002/07/owl#Restriction>} .
 {
  <http://www.agfa.com/w3c/euler/owl-rules#rule10c4>.
  {?r = <http://www.w3.org/2002/03owlt/cardinality/premises005#c>. ?p
= <http://www.w3.org/2002/03owlt/cardinality/premises005#p>. ?r
owl:onProperty ?p} log:implies
{<http://www.w3.org/2002/03owlt/cardinality/premises005#c> owl:onProperty
<http://www.w3.org/2002/03owlt/cardinality/premises005#p>} .
  {?r = <http://www.w3.org/2002/03owlt/cardinality/premises005#c>. ?m = "1"
^^<http://www.w3.org/2001/XMLSchema#nonNegativeInteger>. ?r owl:cardinality
?m} log:implies {<http://www.w3.org/2002/03owlt/cardinality/premises005#c>
owl:cardinality "1"^^<http://www.w3.org/2001/XMLSchema#nonNegativeInteger>}
.
  ?v540994 = <http://www.w3.org/2002/03owlt/cardinality/premises005#c>.
?v540994 <http://www.w3.org/2002/07/owl#maxCardinality> "1"
^^<http://www.w3.org/2001/XMLSchema#nonNegativeInteger>} log:implies
{<http://www.w3.org/2002/03owlt/cardinality/premises005#c>
<http://www.w3.org/2002/07/owl#maxCardinality> "1"
^^<http://www.w3.org/2001/XMLSchema#nonNegativeInteger>} .
{?v540994 = <http://www.w3.org/2002/03owlt/cardinality/premises005#c>.
?v540994 <http://www.w3.org/2002/07/owl#onProperty>
<http://www.w3.org/2002/03owlt/cardinality/premises005#p>} log:implies
{<http://www.w3.org/2002/03owlt/cardinality/premises005#c>
<http://www.w3.org/2002/07/owl#onProperty>
<http://www.w3.org/2002/03owlt/cardinality/premises005#p>} .

Received on Sunday, 6 April 2003 09:20:49 UTC