Re: firts and rdf:rest as functional property

On Mar 20, 2009, at 3:36 PM, Michael Schneider wrote:

> [Originally private discussion between Chris Mungall and me, but Chris
> agreed to forward this to the list. Chris' original mail is quoted.]
>
>
> Hi, Chris!
>
> Thanks for this interesting example! See below for my answer.
>
>> -----Original Message-----
>> From: Chris Mungall [mailto:cjm@berkeleybop.org]
>> Sent: Friday, March 20, 2009 7:37 PM
>> To: Michael Schneider
>> Subject: Re: firts and rdf:rest as functional property
>>
>>
>> On Mar 20, 2009, at 10:43 AM, Pat Hayes wrote:
>>
>>>>>>
>>>>>> (2) Lists should not be cyclic, though this is possible with RDF
>>>>>> lists:
>>>>>>
>>>>>>    A -> B
>>>>>>    ^    |
>>>>>>    |    v
>>>>>>    D <- C
>>>>
>>>> Try to express such a general cycle prohibition axiom! This would
>>>> roughly
>>>> need to say something like:
>>>>
>>>> For any non-negative integer n:
>>>>  there must not be nodes x1,...,xn
>>>>  such that
>>>>     x1 rdf:rest x2
>>>>     x2 rdf:rest x3
>>>>     ...
>>>>     xn rdf:rest x1
>>>>
>>>> If the cycle size would be restricted, one could express this by a
>>>> finite
>>>> set of axioms (I'm not necessarily talking about OWL here). But the
>>>> cycles
>>>> may be arbitrarily large, so this is not possible.
>>
>> possibly missing something,
>> but would this not work (OWL Full issues
>> not withstanding, just taking 'rest' as a standard object property)?
>>
>> SubPropertyOf(rest,restT)
>> Transitive(restT)
>> SubClassOf(HasSelf(restT),owl:Nothing)
>>
>> I thought the main point of HasSelf was to to express simple cyclic
>> structures, e.g. carbon rings
>
> Ok, in principle, this does the job, however...
>
> Here is, how I would prove this.
>
> Claim: Any ontology that is consistent with these axioms does not have
> "rest" cycles.
>
> Assume the contrary:
>
> There exist individuals x1 ... xn such that        (***)
>
>  x1 rest x2 rest ... rest xn rest x1 .
>
> Since rest is a sub property of restT, we also have
>
>  x1 restT x2 restT ... restT xn restT x1 .
>
> Via transitivity of restT, we have
>
>  x1 restT x1
>
> Hence, HasSelf(restT) is non-empty. Contradiction to the third  
> axiom! Q.E.D.
>
> But what have I done? Look at "(***)" above! There is an existential
> assumption about /n/ variables, with non-fixed "n", which means  
> there are in
> fact n existence quantors. This is not a "normal" first order logic  
> proof.
> Instead, one can see this proof in different ways:
>
> (1) As in fact infinitely many different proofs, one for each fixed  
> natural
> number n.
>
> (2) The proof can be seen as saying: "There exists a finite set X =
> {x1,...,xn} of variables...", which means that the existential quantor
> refers to a set --> Second Order Logic!
>
> (3) Alternatively, one can see it to be a single quantor refering to a
> variable of type "finite sequence" <x1,...,xn>. --> Sort of extended  
> First
> Order Logic with arbitrary length tuple-variables.
>
> Dealing with infinitely many proofs (1) is a bit "inconvenient", to  
> say the
> least :). And I think, regarding this as an application of full  
> Second Order
> Logic (2) would be too much, because we only deal with finite  
> enumeration
> sets here. So seeing the proof under the third view is my favorite.  
> I think
> this is what Pat talks about in his earlier mail (I had once a look at
> Common Logic, and found this "sequences as variables" idea there, I
> believe).
>
> Now, after all, it isn't classical first order logic. So something  
> must be
> "wrong" here, because this cannot be expected to be working with at  
> least
> OWL 2 DL. My first guess was that some of the "global restrictions"  
> of OWL 2
> DL are hurt by this example. And, indeed, that's the case:
>
> Look at
>
>
> <http://www.w3.org/2007/OWL/wiki/Syntax#Global_Restrictions_on_Axioms_in_OWL
> _2_DL>
>
> (That's the current Editor's Draft of the "OWL 2 Structural  
> Specification",
> soon to be published as a 2nd Last Call Working Draft).
>
> You can see in Section 11.2, in the paragraph "Restriction on Simple  
> Roles",
> that the constructor "ObjectHasSelf" is listed there. This means  
> that a
> HasSelf restriction may only be applied to so called "simple  
> properties".
> And when you read Section 11.1 (not easy!!!), then you will find out  
> that a
> /transitive/ property is NOT a simple property. So the (non- 
> obvious!) error
> is: You have defined restT to be transitive AND have used it in a  
> HasSelf
> expression. Puh! :)

Ah, I'm familiar with this restriction when it comes to cardinality,  
but I didn't read up thoroughly on HasSelf

It seems that a similar constraint also prohibits:

SubPropertyOf(rest,restT)
Transitive(restT)
Irreflexive(restT)   ***

Perhaps this section of the OWL2 new features and rationale could be  
amended:

http://www.w3.org/TR/2008/WD-owl2-new-features-20081202/ 
#F4:_Self_Restriction

Particularly the example related to monocyclic structures:

	SubClassOf( RingMolecule HasSelf( connectedTo))

I had expected, based on the cited papers by Dumontier et al (which  
uses irreflexivity rather than hasSelf), that connectedTo would be a  
transitive relation holding between for example atoms of a carbon  
ring. I'm no longer sure of the intended real-world meaning of  
connectedTo in the above example.

See:
http://www.w3.org/TR/2008/WD-owl2-new-features-20081202/#Use_Case_.233_-_Classification_of_chemical_compounds_.5BHCLS.5D

> Interestingly, your axioms are valid OWL 2 Full, because the global
> restrictions do not hold for OWL 2 Full. Interesting for me to see  
> that one
> falls out of FOL by doing this.

Interesting

>
> Cheers,
> Michael
>
> --
> Dipl.-Inform. Michael Schneider
> Research Scientist, Dept. Information Process Engineering (IPE)
> Tel  : +49-721-9654-726
> Fax  : +49-721-9654-727
> Email: michael.schneider@fzi.de
> WWW  : http://www.fzi.de/michael.schneider
> = 
> ======================================================================
> FZI Forschungszentrum Informatik an der Universität Karlsruhe
> Haid-und-Neu-Str. 10-14, D-76131 Karlsruhe
> Tel.: +49-721-9654-0, Fax: +49-721-9654-959
> Stiftung des bürgerlichen Rechts, Az 14-0563.1, RP Karlsruhe
> Vorstand: Prof. Dr.-Ing. Rüdiger Dillmann, Dipl. Wi.-Ing. Michael  
> Flor,
> Prof. Dr. Dr. h.c. Wolffried Stucky, Prof. Dr. Rudi Studer
> Vorsitzender des Kuratoriums: Ministerialdirigent Günther Leßnerkraus
> = 
> ======================================================================
>

Received on Tuesday, 24 March 2009 17:54:58 UTC