W3C home > Mailing lists > Public > w3c-rdfcore-wg@w3.org > April 2003

Re: iff

From: pat hayes <phayes@ai.uwf.edu>
Date: Thu, 17 Apr 2003 09:57:33 -0500
Message-Id: <p05111b0bbac46faa3dac@[10.0.100.12]>
To: "Jos De_Roo" <jos.deroo@agfa.com>
Cc: w3c-rdfcore-wg@w3.org

>[following your discussion with Herman]
>
>Although it is the case that
>{{?X rdf:type ?A} => {?X rdf:type ?B}} => {?A rdfs:subClassOf ?B}.
>I fail to see what an engine could ever do with that...
>Suppose it only has following facts loaded
>:Pat rdf:type :Human.
>:Pat rdf:type :American.
>:Peter rdf:type :American.
>does that then mean that it can conclude
>:Human rdfs:subClassOf :American?

No. See below.

>Of course not, as that would be nonmonotonic,
>but what else could it do? What am I missing?

The 'antecedent' of this inference rule amounts to the existence of a 
subproof  of x type B from x type A, with the variable in place. (In 
fact it doesnt have to be a variable, as long as the subproof doesnt 
use any other antecedents which mention the particular subject, since 
then the subject could be changed and the same derivation would 
work); and this entire subproof is the reason this must follow for 
ANY x, hence the final conclusion.

This isn't a closure rule, but it is a valid inference rule. 
Searching for inferences like this make life hard for implementers, 
though, which is why hardly anyone directly implements natural 
deduction systems (except maybe for proof *checkers*). So the task I 
have is to show that this proof rule isnt actually needed since 
rdfs12 covers the only way it could be used, so RDFS can be fully 
captured using only closure rules.

Pat

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


-- 
---------------------------------------------------------------------
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@ai.uwf.edu	          http://www.coginst.uwf.edu/~phayes
s.pam@ai.uwf.edu   for spam
Received on Thursday, 17 April 2003 10:57:37 EDT

This archive was generated by hypermail pre-2.1.9 : Wednesday, 3 September 2003 09:56:57 EDT