From: Michael Schneider <schneid@fzi.de>

Date: Fri, 20 Mar 2009 23:36:31 +0100

Message-ID: <0EF30CAA69519C4CB91D01481AEA06A0011D9B1F@judith.fzi.de>

To: "Chris Mungall" <cjm@berkeleybop.org>, "Semantic Web" <semantic-web@w3.org>

Date: Fri, 20 Mar 2009 23:36:31 +0100

Message-ID: <0EF30CAA69519C4CB91D01481AEA06A0011D9B1F@judith.fzi.de>

To: "Chris Mungall" <cjm@berkeleybop.org>, "Semantic Web" <semantic-web@w3.org>

[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! :) 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. 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 Friday, 20 March 2009 22:37:21 GMT

*
This archive was generated by hypermail 2.3.1
: Tuesday, 26 March 2013 21:45:28 GMT
*