RE: Inferring Properties based on Types

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 Saturday, 29 September 2007 13:16:44 UTC