Re: firts and rdf:rest as functional property

On Mar 20, 2009, at 5: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

Yes, exactly. CL, following KIF, allows for quantification over finite  
sequences. Bu this takes one outside FOL expressivity (unless it is  
VERY carefully syntactically restricted); not all the way into 2nd  
order but into Lw1w, the first infinitary logic. Still way beyond  
description logics, though.

> (I had once a look at
> Common Logic, and found this "sequences as variables" idea there, I
> believe).

Yup.

>
> 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! :)

Which is a bit like taking the exhaust from a jet engine and feeding  
it back into the air intake :-).

>
> 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.

NOt entirely obvious. Some uses of sequence markers are within FOL.  
Basically, you can have them in the antecedent of any entailment you  
are trying to prove, without leaving FOL. In the antecedent they  
simply stand for infinite (but RE) sets of axioms, acting in effect as  
axiom schema. What you can't do (and what you do, in effect, in your  
proof above) is also use them in the consequent. That takes you  
outside FO immediately as it violates compactness.

Chris Menzel and I had a paper in IJCAI2001 on all this, by the way.  
You can get a copy here:

http://philebus.tamu.edu/pipermail/kif/attachments/20010430/a5082884/SKIF-AAAI-format-debug.doc

(The language was being called SKIF rather than CL at that time.) The  
last section outlines the issues concerning "row variables" (as they  
were called then) and FO expressivity.

Pat

>
> 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
> = 
> ======================================================================
>

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

Received on Monday, 23 March 2009 17:16:13 UTC