Re: Inferring Class Membership w/o OWL Full?

On Tuesday, May 11, 2004, at 04:30  PM, Pat Hayes wrote:
>
>> Strangely enough, that is exactly what I told myself when I read your
>> initial email.
>>
>> The point I was trying to make with my [witty banter|vile character
>> assassination]* is that, amusing though your ritual DL bashing is, it
>> obscures the fact that the restriction being discussed here, i.e., not
>> being able to create a subPropertyOf rdf:type, is nothing to do with
>> DLs per se, but is required in order to keep the language inside what
>> I think we agreed to call "conventional" FOL.
>
> I disagree. rdf:type is simply a binary relation. It happens to be 
> related to the operation of unary predication in a systematic way, 
> which can be expressed in SCL-FOL (though not using a syntax that you 
> would honor with the term 'conventional') by the axiom
>
> (iff (rdf:type x y)  (y x) )
>
> and in a more conventional syntax by the axiom
>
> (rdf:type x y) iff (holds y x)
>
> but the special nature of this axiom does not affect the fact that 
> rdf:type is a binary relation. To amplify the point, the operation of 
> creating a subproperty of rdf:type is quite meaningful and has some 
> obvious first-order consequences, such as (using SCL notation and 
> omitting universal quantifiers)
>
> (iff (rdf:type x y)  (y x) )  ...1 (RDF axiom)
> (subProperty foo rdf:type)  ...2
> (implies (subProperty x y) (implies (x z u) (y z u)))  ....3 (RDFS 
> axiom)
> (foo thing class)  ...4
> |=
> (class thing)
>
> proof:
> (implies (foo z u) (rdf:type z u) )  ....5 (3, UInstance; 2, Modus 
> Ponens)
> (rdf:type thing class)  ...6 (5, Uinstance; 4, Modus Ponens)
> (class thing)  (1, conj; Uinstance; 6, Modus Ponens)

Hello Pat,

If this argument is (as it seems to me, anyway) valid, isn't it also 
independent of whether subProperties of rdf:type are definable? That 
is, take the axioms

1. [Subst instance of RDF axiom] y/some_class, x/some_inst
4'. (rdf:type some_inst some_class)
|=
(some_class some_thing)

No? I don't think I am missing your overall point, it's just that your 
point seems to be not essentially related to the definability of 
subproperties. (Incidentally, is rdfs:subProperty not reflexive? Its 
informal explanations in the standards characterize a reflexive 
relation, as far as I can tell - but if so, then 2'. (subProperty 
rdf:type rdf:type).)

Best regards,

> Or you could derive it by unit resolution once the implications and 
> iff were translated into clauses in the usual way. The only thing 
> unconventional about this is that it systematically suppresses the 
> 'holds' relation by allowing variables to occur in predicate position, 
> which does not significantly affect any of the FO metatheory.
>
> My 'DL police' [witty banter|vile character assassination]* was a 
> reference to the fact that OWL-DL (hence the "DL") has been thoroughly 
> checked and constrained so as to not permit a range of modes of 
> expression, and that if something appears to be syntactically illegal 
> by virtue of these rules, the chances of one being able to wriggle 
> past the constraints by some superficial transformations, as Stephen 
> had suggested, are vanishingly low. This remark was in part a 
> testament to the thoroughness of the job done by you and Peter in 
> defining the OWL-DL syntactic conditions, in fact. As you point out, 
> not all these restrictions arise from the need for OWL-DL to be a 
> description logic. Nevertheless, for whatever reason, they have been 
> imposed on the language, and I do not think it is misleading to imply 
> that they were imposed largely at the behest of those who were most 
> enthusiastic about DLs.
....

--
Pierluigi
@home Austin, Tex.

Received on Wednesday, 12 May 2004 23:14:56 UTC