- From: pat hayes <phayes@ai.uwf.edu>
- Date: Thu, 17 Apr 2003 09:57:33 -0500
- 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 UTC