From: Chris Mungall <cjm@berkeleybop.org>

Date: Fri, 20 Mar 2009 16:12:52 -0700

Cc: "Semantic Web" <semantic-web@w3.org>

Message-Id: <5CD69604-8B13-4C85-B453-C6B33843747F@berkeleybop.org>

To: "Michael Schneider" <schneid@fzi.de>

Date: Fri, 20 Mar 2009 16:12:52 -0700

Cc: "Semantic Web" <semantic-web@w3.org>

Message-Id: <5CD69604-8B13-4C85-B453-C6B33843747F@berkeleybop.org>

To: "Michael Schneider" <schneid@fzi.de>

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 GMT

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