From: Michael Schneider <schneid@fzi.de>

Date: Sat, 29 Sep 2007 15:16:30 +0200

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

To: "Ian Horrocks" <horrocks@cs.man.ac.uk>

Cc: "Swanson, Tim" <tim.swanson@semanticarts.com>, "Owl Dev" <public-owl-dev@w3.org>

Date: Sat, 29 Sep 2007 15:16:30 +0200

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

To: "Ian Horrocks" <horrocks@cs.man.ac.uk>

Cc: "Swanson, Tim" <tim.swanson@semanticarts.com>, "Owl Dev" <public-owl-dev@w3.org>

Hello, Ian! Ian Horrocks wrote on September 16, 2007: >On 15 Sep 2007, at 23:18, Michael Schneider wrote: > >> >> Hi, Tim! >> >>> -----Original Message----- >>> From: public-owl-dev-request@w3.org >>> [mailto:public-owl-dev-request@w3.org] On Behalf Of Swanson, Tim >>> Sent: Saturday, September 15, 2007 12:18 AM >>> To: public-owl-dev@w3.org >>> Subject: Inferring Properties based on Types >>> >>> >>> Is there any way in OWL (or in any of the proposed extensions) to >>> express an inference rule like the following: >>> >>> (?x :P ?y) >>> :A(?y) >>> => >>> (?x :R ?y) >>> >>> >>> For a more concrete example: >>> >>> (?x :hasSibling ?y) >>> :Male(?y) >>> => >>> (?x :hasBrother ?y) > >It isn't possible in either OWL or OWL 1.1. This is a late response, but it kept me wondering, if there is an easy to understand reason for /why/ Tim's rule (R1) FORALL x,y: sibling(x,y) AND Man(y) ==> brother(x,y) is not possible to express in OWL-1.1. Now, I finally found the time to think about this question more deeply. And, to my surprise, it seems to me that there still is a way to make it happen. Can this be the case? My idea is trying to simulate the class 'Man(.)' by a role 'manman(.,.)', which is intended to "behave equivalently" to 'Man'. I formalize this idea by the the following set of two statements: (S1) FORALL x: manman(x,x) <==> Man(x) (S2) FORALL x,y: manman(x,y) ==> x = y By (S1), I try to express that there is a "natural" one-to-one correspondence between instances of class 'Man', and "loop" instances of role 'manman' (by "loop" I mean role instances of the form 'manman(x,x)'). And (S2) is meant to express that (S1) already fully specifies the 'manman' role. Using (S1), I can restate Tim's original rule (R1) in the following way: (R2) FORALL x,y: sibling(x,y) AND manman(y,y) ==> brother(x,y) And I claim (see below for my argumentation) that from (S2) it follows that (R2) is equivalent to: (R3) FORALL x,y: [ EXISTS z: sibling(x,z) AND manman(z,y) ] ==> brother(x,y) Then, (R3) can be translated into an OWL-1.1 "sub property chain": (R4) SubObjectPropertyOf( SubObjectPropertyChain(sibling manman) brother ) And as you told me in a previous mail about the "uncle" problem, I am really allowed to build such complex sub role chains, where the super role, 'brother' here, may be different from the chained roles, 'sibling' and 'manman' here. BTW: In this mail, I will always use for OWL-Axioms the (hopefully :)) most current functional syntax and semantics as specified in [1]. So, /if/ my simulation of class 'Man' by role 'manman' is adequate, and /if/ I were able to translate the statement set {(S1),(S2)} into an equivalent OWL-1.1 axiom set {A1,...,An}, /then/ I were able to express Tim's rule (R1) as the OWL-1.1 axiom set {(R4),A1,...,An}. Before I further discuss this question, I will first try to give an argument for my claim that from (S2) I can infer the equivalence of (R2) and (R3). For this to be true, AFAICS it suffices to show that the predicates p and q, defined by p(x,y) := sibling(x,y) AND manman(y,y) q(x,y) := EXISTS z: sibling(x,z) AND manman(z,y) are equal under the condition (S2). This seems to be the case: * Case "(S2) ==> FORALL x,y: [p(x,y) ==> q(x,y)]": Given arbitrary instances x and y, for which sibling(x,y) and manman(y,y) both hold. I define z := y, which provides me the existence of some z, for which both sibling(x,z) and manman(z,y) hold. (Note that this direction of the argument did not even use condition (S2)). * Case "(S2) ==> FORALL x,y: [q(x,y) ==> p(x,y)]": Given arbitrary instances x and y, and let's further assume that some instance z exists, for which sibling(x,z) and manman(z,y) both hold. Then we can conclude from (S2) that z = y. Hence, both sibling(x,y) and manman(y,y) hold. Thus, (R2) and (R3) really seem to be equivalent within the context of the statement set {(S1),(S2)}. So the remaining question is: Can I express the statement set {(S1),(S2)} in OWL-1.1 ? First, I split (S1) into the equivalent statement set (S1a) FORALL x: Man(x) ==> manman(x,x) (S1b) FORALL x: manman(x,x) ==> Man(x) Next, I claim that the statement set {(S1b),(S2)} is equivalent to the statement set {(S1b'),(S2)}, where (S1b') is given by: (S1b') FORALL x: [ EXISTS y: manman(x,y) ] ==> Man(x) Again, it suffices to show that the predicates P and Q, defined by P(x) := manman(x,x) Q(x) := EXISTS y: manman(x,y) are equal under the condition (S2). The argumentation for this is pretty analog to the argumentation for the "(S2) ==> [(R2) <==> (R3)]" claim above. Well, I won't perform this a second time. :) So what I have to do now is to find a set of OWL-1.1 axioms, which are equivalent to the following set of three statements: (S1a) FORALL x: Man(x) ==> manman(x,x) (S1b') FORALL x: ( EXISTS y: manman(x,y) ) ==> Man(x) (S2) FORALL x,y: manman(x,y) ==> x = y Here is my proposed set of OWL-1.1 axioms: (A1) SubClassOf( Man ObjectExistsSelf(manman) ) (A2) SubClassOf( ObjectMinCardinality(1 manman owl:Thing) Man ) (A3) ObjectPropertyDomain( manman Man ) (A4) FunctionalObjectProperty( manman ) First, I deduce all statements from the axiom set: * Deduction of (S1a): (A1) is the equivalent translation of (S1a), because 'ObjectExistsSelf(R)' denotes the class {x:R(x,x)}. * Deduction of (S1b'): (A2) is the equivalent translation of (S1b'), because 'ObjectMinCardinality(1 R owl:Thing)' denotes the class {x: #{y:R(x,y)} >= 1}. * Deduction of (S2): Given arbitrary instances x and y, for which manman(x,y) holds. So, x is in the domain of manman. Thus, from (A3) it follows that Man(x) holds. This allows me to conclude from (A1) that manman(x,x) also holds. And by (A4), I get (x,y) = (x,x), hence x = y. Second, I deduce all axioms from the statement set: * Deduction of (A1): (A1) is the equivalent translation of (S1a). * Deduction of (A2): (A2) is the equivalent translation of (S1b'). * Deduction of (A3): From (S1a), I learn that for each Man x there exists a role instance manman(x,.), thus Man is a subset of domain(manman). >From (S1b') I learn that whenever there is some role instance manman(x,.), then x is a Man, thus domain(manman) is a subset of Man. Hence domain(manman) = Man. * Deduction of (A4): Given arbitrary instances x, y and z, for which manman(x,y) and manman(x,z) both hold. From (S2) it follows x = y, and x = z. Hence y = z, i.e. manman is a functional role. So, it turnes out that the statement set {(S1a),(S1b'),(S2)} is equivalent to the OWL-1.1 axiom set {(A1),(A2),(A3),(A4)}. And I showed before that {(S1a),(S1b'),(S2)} is equivalent to {(S1),(S2)}. And the latter statement set had made it possible to express (R1) in the form of the OWL-1.1 axiom (R4). So it seems to me that Tim's rule really is expressable in OWL-1.1, as the axiom set { (R4), (A1), (A2), (A3), (A4) } (Tim's Rule expressed in OWL-1.1) Did I make a mistake anywhere? Cheers, Michael [1] http://www.webont.org/owl/1.1/semantics.html#2 >The "work-around" given below by Michael is similar to what you would >get be using a suitable DL-safe rule -- intuitively, this is a rule >of a form such that it will only affect named individuals. An >arbitrary rule (such as the one you give above) can be transformed >into a DL-safe one by introducing a new unary predicate, say >NamedIndividual, that is true for all named individuals (this can be >achieved by adding the ground fact => NamedIndividual(i) for every >individual i occurring in the ontology), and by adding atoms >NamedIndividual(?v) to the body of the rule for each variable ?v used >in the rule. > >Of course using a DL-safe rule (or equivalently Michael's work- >around) with an ontology O will *not* (by itself) result in >entailments such as the class of people having a male sibling being a >subclass of the class of people having a brother. > >Regards, >Ian > > >> >> I think, you can at least do the following: >> >> First, use the inverses of the roles 'hasSibling(.,.)' and >> 'hasBrother(.,.)', called 'isSiblingOf(.,.)' and isBrotherOf(.,.)', >> respectively. >> >> With this, the following rule is equivalent to yours: >> >> (1) isSiblingOf(y,x), Man(y) => isBrotherOf(y,x) >> >> This can be transformed into: >> >> (2) y IN {z|isSiblingOf(z,x)} AND Man(y) => y IN >{z|isBrotherOf(z,x)} >> >> And this translates (and generalizes) into the following OWL/DL >> (1.0) axiom: >> >> (3) SubClassOf( >> intersectionOf( >> restriction( isSiblingOf value(x) ) >> Class(Man) >> ) >> Restriction( isBrotherOf value(x) ) >> ) >> >> Problem with this approach: You need one such axiom for each >> individual x >> (the variable 'x' appears free in (2)). >> >> Cheers, >> Michael >> >> >> -- >> Dipl.-Inform. Michael Schneider >> FZI Forschungszentrum Informatik Karlsruhe >> Abtl. Information Process Engineering (IPE) >> Tel : +49-721-9654-726 >> Fax : +49-721-9654-727 >> Email: Michael.Schneider@fzi.de >> Web : http://www.fzi.de/ipe/eng/mitarbeiter.php?id=555 >> >> 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 Regierungspräsidium Karlsruhe >> Vorstand: Rüdiger Dillmann, Michael Flor, Jivka Ovtcharova, Rudi >> Studer >> Vorsitzender des Kuratoriums: Ministerialdirigent Günther Leßnerkraus >> > > -- Dipl.-Inform. Michael Schneider FZI Forschungszentrum Informatik Karlsruhe Abtl. Information Process Engineering (IPE) Tel : +49-721-9654-726 Fax : +49-721-9654-727 Email: Michael.Schneider@fzi.de Web : http://www.fzi.de/ipe/eng/mitarbeiter.php?id=555 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 Regierungspräsidium Karlsruhe Vorstand: Rüdiger Dillmann, Michael Flor, Jivka Ovtcharova, Rudi Studer Vorsitzender des Kuratoriums: Ministerialdirigent Günther LeßnerkrausReceived on Saturday, 29 September 2007 13:16:44 GMT

*
This archive was generated by hypermail 2.3.1
: Wednesday, 27 March 2013 09:32:55 GMT
*