From: Michael Schneider <schneid@fzi.de>

Date: Sun, 7 Oct 2007 12:14:07 +0200

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

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

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

Date: Sun, 7 Oct 2007 12:14:07 +0200

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

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

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

Hi, Ian! Ian Horrocks wrote: >Thanks for pointing out my error in asserting that it wasn't possible >to express Tim's rule in OWL 1.1. > >Now you have pointed out the basic trick, I wonder why the set of >axioms for expressing this rule is so complex. In particular, why do >we need it to be the case that manman(x,x) <=> Man(x) -- wouldn't it >be enough that Man(x) => manman(x,x)? I think this condition would be too weak, because it would allow the 'manman' role to take many different shapes without hurting this condition. For example, the /identity/ relationship id(x,x) :<=> x=x would be allowed for the 'manman' role by such a condition. And more generally, every role which is reflexive would also be allowed, so for instance the "full" role "owl:Thing X owl:Thing" could then be used as the 'manman' role. This would have the potential of introducing problems, I believe. >We could also do without >reflexivity -- we could simply use an existential restriction to >force the existence of *some* manman relation and then use (sibling >manman InverseObjectProperty(manman)) as the role chain implying >brother. This would give: > >SubClassOf(Man ObjectExists(manman Thing)) >SubObjectPropertyOf(SubObjectPropertyChain(sibling manman >InverseObjectProperty(manman)) brother) The first axiom here will be consistent with any model that uses for 'manman' a role r, which for each Man x ensures the existence of some instance y so that r(x,y) holds. For example, manman := id would be a permitted role by this first axiom, because id(x,x) holds for every instance x, so especially it holds for each Man x, and by setting y := x we get the existence of some instance y with id(x,y). Hence, for each Man x there is some instance y with manman(x,y). But by choosing the identity relationship as the 'manman' role, we can do the following inference starting from the second axiom: SubObjectPropertyOf(SubObjectPropertyChain( sibling manman InverseObjectProperty(manman)) brother) |= SubObjectPropertyOf(SubObjectPropertyChain( sibling id InverseObjectProperty(id)) brother) |= SubObjectPropertyOf(SubObjectPropertyChain( sibling id)) brother) |= SubObjectPropertyOf(sibling brother) And this is certainly not what we intended to get, because suddenly every sibling is a brother, without needing to check if it also is a Man. And when we select for instance manman := "owl:Thing X owl:Thing", which is also allowed by the first axiom above, then we may even get more unintended brothers. Note that with my original two conditions FORALL x: Man(x) <=> manman(x,x) FORALL x,y: manman(x,y) => x=y the situation "manman = id" can also occur, but only with models for which Man = owl:Thing. And in *this* specific case it is really true that every sibling is also a brother. But I tried to choose my two conditions in a way, which allows me to deal with *every* case, i.e. with models having arbitrary extensions of class Man. I did this by trying to specify my 'manman' role in the most restrictive way which I could think of, so that unintended interpretations for 'manman' are not possible. At least, it seems that I can show that under my two conditions, the 'manman' role is /uniquely/ specified with respect to a given model: Let 'manman1' and 'manman2' be two roles for which the above two conditions hold. Let's start with two arbitrary instances x and y, for which manman1(x,y) is true. Then from the second condition we receive x=y, so manman1(x,x) is true. From the first condition we then get Man(x). And because 'manman2' also matches the two conditions, we get manman2(x,x) from the first condition. But we had x=y, so finally manman2(x,y) is true. The other direction of this equality proof is performed analog. 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ßnerkrausReceived on Sunday, 7 October 2007 10:14:23 GMT

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