Re: rdf:first/rest/nil/List: syntax-only at the RDF level

[...]

> Now... webont's use of first/rest would seem to need these.
> But it doesn't. I agree that it needs
> this:
>
>   eg:C1 owl:intersectionOf _:these.
>   _:these rdf:first eg:A.
>   _:these rdf:first eg:B.
> ==>
>   eg:A owl:sameAs eg:B.
>   eg:A owl:sameClassAs eg:B.
>
> As I proposed[23Oct] to WebOnt, this follows because
> the range of owl:intersectionOf is a class, owl:List,
> which is specified to have maxCardinality 1 for rdf:first
> and rdf:rest.
>
> Hmm... this seems straightforward, but maybe it's worth working
> out the details... (yes, found one bug: I was
> saying cardinality, but I meant maxCardinality... fixed that...).
> OK, worked out the details:
>
> http://www.w3.org/2000/10/swap/test/list/listlayerP.n3
> http://www.w3.org/2000/10/swap/test/list/listlayerC.n3
>
> Jos, I was gonna test that with Euler to show the proof,
> but my Euler installation seems to have fallen apart.
> Would you mind?

glad to test such cases...
it took me quite a while, but I now find (*) that

==== listlayerP
@prefix owl: <http://www.w3.org/2002/07/owl#> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix eg: <http://example/vocab#>.

eg:C1 owl:intersectionOf _:these .
_:these rdf:first eg:A .
_:these rdf:first eg:B .
====

=>

==== listlayerC
@prefix owl: <http://www.w3.org/2002/07/owl#> .
@prefix eg: <http://example/vocab#>.

eg:A owl:equivalentTo eg:B.
eg:A owl:sameClassAs eg:B.
====


we had to update http://www.agfa.com/w3c/euler/owl-rules
with

owl:List rdfs:subClassOf [ owl:onProperty rdf:first; owl:maxCardinality "1"
] .

and

{ :rule6e4 . ?r owl:onProperty ?p . ?r owl:maxCardinality "1" . ?s ?p ?x .
?s ?p ?y . ?s a ?r } log:implies { ?x owl:equivalentTo ?y } .

(and we also had to remove a kind of ALL
(Access Limited Logic) feature that we
experimented with for searchspace pruning
so we now have a bit more steps...)

for the rest I think that owl:List is making sense

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

(*)
java Euler -local listlayerP http://www.w3.org/2002/07/owl listlayerC
# Generated with http://www.agfa.com/w3c/euler/#R3226 on 26 Oct 2002
14:47:56 GMT
# for query file:/www.w3.org/2000/10/swap/test/list/listlayerC.n3
# given {file:/www.w3.org/2000/10/swap/test/list/listlayerP.n3=[],
http://www.agfa.com/w3c/euler/owl-rules.n3=[]}

@prefix str: <http://www.w3.org/2000/10/swap/string#> .
@prefix ns: <http://www.agfa.com/w3c/euler/rdfs-rules#> .
@prefix xsd: <http://www.w3.org/2001/XMLSchema#> .
@prefix : <http://www.agfa.com/w3c/euler/owl-rules#> .
@prefix eg: <http://example/vocab#> .
@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 rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .

 {
  <http://www.agfa.com/w3c/euler/owl-rules#rule6e4> .
  _:6818393_2 owl:onProperty rdf:first.
  _:6818393_2 owl:maxCardinality "1".
   {
    <http://www.agfa.com/w3c/euler/rdfs-rules#rule9> .
    owl:List rdfs:subClassOf _:6818393_2.
     {
      <http://www.agfa.com/w3c/euler/rdfs-rules#rule3> .
      owl:intersectionOf rdfs:range owl:List.
      eg:C1 owl:intersectionOf _:these_1} log:implies
    {_:these_1 a owl:List}} log:implies
  {_:these_1 a _:6818393_2}.
  _:these_1 rdf:first eg:A.
  _:these_1 rdf:first eg:B} log:implies
{eg:A owl:equivalentTo eg:B}.
eg:A owl:sameClassAs eg:B.

<http://example/vocab#B> <http://www.w3.org/2002/07/owl#equivalentTo>
<http://example/vocab#A> .

# Proof found for file:/www.w3.org/2000/10/swap/test/list/listlayerC.n3 in
3040 steps (20585 steps/sec) using 1 engine

Received on Saturday, 26 October 2002 11:06:40 UTC