Re: Inferring Properties based on Types

[reply to the list this time]

On 10/1/07, Evren Sirin <evren@clarkparsia.com> wrote:

[skip]

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).


I think this wouldn't work as expected. To be more precise, it would
silently introduce additional restrictions to the model. As the semantics of
the construction
          ReflexiveObjectProperty( manman )
is the following GCI
          SubClassOf ( owl:Thing ObjectExistsSelf(manman) )
and we have a domain of the property manman, than the (implicit) axiom
          SubClassOf (owl:Thing, Man)
would be added to the ontology. The same would happen for every other
reflexive property with either range or domain defined. So, every concept in
the ontology would be a Man (in addition to all other supertypes).

Best,
Dmitry.

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.1axiom
> > (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
> >
> >
>
>
>