Re: Inferring Properties based on Types

Hi Michael,
Your suggestion is a nice trick that almost works! In summary, you are 
saying we can use the following set of OWL 1.1 axioms

>     (R4) SubObjectPropertyOf( SubObjectPropertyChain(sibling manman) brother)
>
>     (A1) SubClassOf( Man ObjectExistsSelf(manman) )
>     (A2) SubClassOf( ObjectMinCardinality(1 manman owl:Thing) Man )
>     (A3) ObjectPropertyDomain( manman Man )
>     (A4) FunctionalObjectProperty( manman )
>   
to express the rule

> (?x :hasSibling ?y) ^ :Male(?y) => (?x :hasBrother ?y)

I think your set of axioms would do the trick but there is one problem. 
A1 together with A4 violates the non-structural restrictions on axioms 
as explained in [1]. The same property cannot be both used in an 
ObjectExistsSelf restriction and FunctionalObjectProperty axiom (or any 
other cardinality expression). However, same restriction does not apply 
to ReflexiveObjectProperty which could be used in place of 
ObjectExistsSelf in this situation. Also note that A2 is redundant since 
it is semantically equivalent to A3. With these modifications we get the 
following set of axioms to express the above rule in OWL 1.1:

    (R4) SubObjectPropertyOf( SubObjectPropertyChain(sibling manman) brother)
    (A1') ReflexiveObjectProperty( manman )
    (A3) ObjectPropertyDomain( manman Man )
    (A4) FunctionalObjectProperty( manman )


One could possibly define a macro that would translate a user-friendly 
syntax into this set of axioms (and would generate the a unique property 
like manman for different uses).

There is a slight problem with this encoding. Since we defined a complex 
subproperty for the property brother, there are some restrictions on its 
usage (again [1]), e.g. it cannot be used in cardinality restrictions 
anymore.

Cheers,
Evren

[1] http://webont.org/owl/1.1/owl_specification.html#7


On 9/29/07 9:16 AM, Michael Schneider wrote:
> 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ßnerkraus
>
>

Received on Monday, 1 October 2007 14:30:19 UTC