Re: entailment-from-inconsistent-graph [was: proposed test of RDFS entailment rules]

>[is redirected from rdf-comments to rdf-core]
>
>Pat - that * suggestion is actually a very good one.
>I've done a small test (just this particular case but
>it could be generalized to all XML clashes and
>maybe also other datatype clashes, but then we
>need a bit more time to write code to invoke
>XML parsers and/or datatype checkers).
>The results are reflected in following proof
>
>[[
>@prefix iw: <http://www.ksl.stanford.edu/software/IW/spec/iw#>.
>@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.org/eg#>.
>  {
>   <http://www.agfa.com/w3c/euler/rdfs-rules#rdfs9>.
>    {[iw:Variable "?A"] = rdf:XMLLiteral.
>     [iw:Variable "?B"] = rdfs:Literal.
>     [iw:Variable "?A"] rdfs:subClassOf [iw:Variable "?B"]} =>
>   {rdf:XMLLiteral rdfs:subClassOf rdfs:Literal}.
>    {
>     <http://www.agfa.com/w3c/euler/rdfs-rules#rdfs3>.
>      {[iw:Variable "?P"] = eg:prop.
>       [iw:Variable "?C"] = rdf:XMLLiteral.
>       [iw:Variable "?P"] rdfs:range [iw:Variable "?C"]} =>
>     {eg:prop rdfs:range rdf:XMLLiteral}.
>      {[iw:Variable "?S"] = eg:foo.
>       [iw:Variable "?P"] = eg:prop.
>       [iw:Variable "?O*"] = "<"^^rdf:XMLLiteral.
>       [iw:Variable "?S"] [iw:Variable "?P"] [iw:Variable "?O*"]} =>
>     {eg:foo eg:prop "<"^^rdf:XMLLiteral}.
>     [iw:Variable "?S*"] = "<"^^rdf:XMLLiteral.
>     [iw:Variable "?A"] = rdf:XMLLiteral.
>     [iw:Variable "?S*"] a [iw:Variable "?A"]} =>
>   {"<"^^rdf:XMLLiteral a rdf:XMLLiteral}.
>   [iw:Variable "_:Y_3*"] = "<"^^rdf:XMLLiteral.
>   [iw:Variable "_:Y_3*"] a rdfs:Literal} =>
>{"<"^^rdf:XMLLiteral a rdfs:Literal}.
>]]
>
>in which you should see 6 occurences of *'ed variables
>and an appropriate proof checker is informed that way.
>
>Till now, I made separate rules to derive inconsistencies
>but maybe this way is better; any further thoughts??

I think this way works fine and should extend to 
datatype clashes in a uniform way, though the 
derivations there will require datataype savvies 
of course.

The archetype datatype contradiction would be something of the form
"literalForm"^^ex:datatype a ex:otherDatatype
where the "LiteralForm" cannot denote something 
in the value space of ex:otherDatatype (for any 
number of reasons, the most obvious being that it 
is illtyped for ex:datatype, but in particular 
cases it could include things like
"0.3"^^xsd:real a xsd:integer .
where the literal is well-typed in itself, so is 
a kosher  rdfs:Literal,  but is an 'illegal' 
value for the target datatype.

I think this is the most general case possible in 
RDFS+D, but I havn't worked it out in full 
detail.  In OWL you can get other datatype 
contradictions, eg by defining a subclass of 
xsd:boolean with three distinct things in it.

Pat

>
>--
>Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
>
>
> 
>                                                                                                                                        
>                       pat 
>hayes                                                                                                          
>                       <phayes@ihmc.us> 
>To:       Jos 
>De_Roo/AMDUS/MOR/Agfa-NV/BE/BAYER@AGFA                                   
>                       Sent by: 
>cc:       "Peter F. Patel-Schneider" 
><pfps@research.bell-labs.com>,                    
>                       www-rdf-comments-req 
>www-rdf-comments@w3.org, 
>www-rdf-comments-request@w3.org                              
>                       uest@w3.org 
>Subject:  Re: entailment-from-inconsistent-graph 
>[was: proposed test of  RDFS          
> 
>entailment 
>rules]                                                                    
> 
>                                                                                                                                        
>                       2003-10-18 03:18 
>PM                                                                                                
> 
>                                                                                                                                        
> 
>                                                                                                                                        
>
>
>
>
>
>The current (editor's draft) RDFS rules have a
>criterion for detecting inconsistency, to wit,
>the derivation of a triple called an 'XML clash'.
>
>_:nnn rdf:type rdfs:Literal .
>
>where the subject bnode _:nnn was introduced, and
>allocated to an ill-typed literal by, the lg
>generalization rule (formerly called rdf2). The
>derivation for this example is as follows:
>
><http://example.org/prop>
><http://www.w3.org/2000/01/rdf-schema#range>
><http://www.w3.org/1999/02/22-rdf-syntax-ns#XMLLiteral>
>.
>
><http://example.org/foo>
><http://example.org/prop>
>"<"^^<http://www.w3.org/1999/02/22-rdf-syntax-ns#XMLLiteral>
>.
>
><http://example.org/foo>
><http://example.org/prop> _:1*.      rule lg,
>with _:1* allocated to
>"<"^^<http://www.w3.org/1999/02/22-rdf-syntax-ns#XMLLiteral>,
>which is ill-typed. (Jos, can your code keep
>track of this when the rule is applied and 'mark'
>the bnode accordingly?)
>
>_:1*
><http://www.w3.org/1999/02/22-rdf-syntax-ns#type>
><http://www.w3.org/1999/02/22-rdf-syntax-ns#XMLLiteral> .   rule rdfs3
>
><http://www.w3.org/1999/02/22-rdf-syntax-ns#XMLLiteral>
><http://www.w3.org/2000/01/rdf-schema#subClassOf>
><http://www.w3.org/2000/01/rdf-schema#Literal> .
>RDFS axiomatic triple
>
>_:1* <http://www.w3.org/1999/02/22-rdf-syntax-ns#type>
><http://www.w3.org/2000/01/rdf-schema#Literal>  .               rule rdfs9
>
>So the 'ex cont quod' could reasonably be
>restricted to this case, ie if you really believe
>an XML clash then you will believe anything.
>However, notice that the clash itself is not
>inconsistent: it is a symptom of the original set
>being inconsistent. So it would not be correct to
>say that the silly conclusion is entailed by the
>clash; rather, if you can derive a clash from a
>graph, then  the silly conclusion is entailed by
>your original graph.
>
>>What a coincidence - while sitting in a plane this evening
>>I did't think to implement a "ex contradictione quodlibet".
>>The premise graphs are assumed to be the case unless they
>>can be proven to be inconsistent and then we just say so
>>and don't explicitly use them further. So we can't
>>run that testcase.
>
>I think it would be OK to be able to prove the
>antecedent inconsistent, and call that a proper
>run of the test-case. I think that was Peter's
>main point.
>
>Pat
>
>>
>>
>>--
>>Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
>>
>>
>>
>>
>
>>                        Brian
>>McBride
>
>>                        <bwm@hplb.hpl.hp.com
>>To:       "Peter F. Patel-Schneider"
>><pfps@research.bell-labs.com>
>>                        >
>>cc:
>>www-rdf-comments@w3.org
>
>>                       Sent by:
>>Subject:  entailment-from-inconsistent-graph
>>[was: proposed test of RDFS entailment
>>                        www-rdf-comments-req
>>rules]
>
>>
>>uest@w3.org
>
>>
>>
>
>>
>>
>
>>                        2003-10-15 03:37
>>PM
>
>>
>>
>
>>
>>
>
>>
>>
>>
>>
>>
>>Peter,
>>
>>The WG were unable to discuss this suggestion before publishing the 2nd
>>last call documents.  I propose to track this as a 2nd last call comment:
>>
>>http://www.w3.org/2001/sw/RDFCore/20031010-comments/#entailment-from-inconsistent-graph
>
>>
>>
>>Brian
>>
>>
>>
>>
>>Peter F. Patel-Schneider wrote:
>>>   I propose that the following be a positive entailment test in the RDF
>>test
>>>   suite.  This is a valid RDFS entailment (modulo typing errors), but is
>>not
>>>   a consequence of the current RDFS entailment rules.
>>>
>>>   Premise
>>>
>>   > <http://example.org/prop> <http://www.w3.org/2000/01/rdf-schema#range>
><
>>http://www.w3.org/1999/02/22-rdf-syntax-ns#XMLLiteral> .
>>>   <http://example.org/foo> <http://example.org/prop> "<"^^<
>>http://www.w3.org/1999/02/22-rdf-syntax-ns#XMLLiteral> .
>>   >
>>>   Conclusion
>>>
>>>   <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <
>>http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <
>  >http://www.w3.org/1999/02/22-rdf-syntax-ns#type> .
>>>
>>>
>>>   Peter F. Patel-Schneider
>
>
>--
>---------------------------------------------------------------------
>IHMC         (850)434 8903 or (650)494 3973   home
>40 South Alcaniz St.           (850)202 4416   office
>Pensacola                                  (850)202 4440   fax
>FL 32501                                   (850)291 0667    cell
>phayes@ihmc.us       http://www.ihmc.us/users/phayes


-- 
---------------------------------------------------------------------
IHMC	(850)434 8903 or (650)494 3973   home
40 South Alcaniz St.	(850)202 4416   office
Pensacola			(850)202 4440   fax
FL 32501			(850)291 0667    cell
phayes@ihmc.us       http://www.ihmc.us/users/phayes

Received on Monday, 27 October 2003 13:19:39 UTC