Re: ISSUE-3: REPORTED: Lack of anonymous individuals

[Resending my previous note with the ISSUE subject line so tracker  
keeps a pointer to it]

A discussion with Ian about the difference between anonymous  
individuals and skolems

Begin forwarded message:
From: Ian Horrocks <horrocks@cs.man.ac.uk>
Date: August 29, 2006 10:43:52 AM EDT
To: Alan Ruttenberg <alanruttenberg@gmail.com>
Subject: Re: anonymous individual

On 26 Aug 2006, at 06:36, Alan Ruttenberg wrote:

I'm still missing something but I'm not sure it's sensible - you be  
the judge.

If I understand your example you are saying that if (a) and (b) mean  
the same thing, then you can replace one with the other. Therefore  
(a) , not(b) should be able to be rewritten as  (b) ,  not(a) by  
swapping (a) and (b) in the axioms. Then you show that these are not  
equivalent, since one is satisfiable and the other not, and so (a)  
and (b) can't mean the same thing.

Exactly.


I'm trying to compare this to what I considered the more obvious way  
to showing that they are different.

Fair enough.


If the blank node and the skolemized version are to have different  
meanings, then it seems that the challenge would be:

I tell you  that I plan to add either of these two axioms

(a) individual(John value(hasFriend individual(value(hasFriend  
Jane)))) or
(b) individual(John value(hasFriend individual(<somename> value 
(hasFriend Jane))))

I don't tell you the name I will use for  <somename> since it can't  
be known to you anyways - it's a fresh name.

You give me a set of axioms (c) such that if I add (a) the ontology  
is either satisfiable or not but if I add (b) then the ontology is  
the opposite (unsatisfiable if adding (a) made it satisfiable,  
satisfiable if adding (a) made it unsatisfiable)

I do see your point about (b) having fewer models than (a). Given  
that, it seems clear that the challenge will be that (a) added to (c)  
is satisfiable, but (b) added to (c) is not, rather than the two  
choices I listed above.

What's not obvious to me is whether the in the illustration you give  
using two ontologies necessarily mean that one can construct a single  
set of axioms (c) that rules out all the models that (b) allows  
(without knowing what <somename> is) while leaving in place some of  
the ones that (a) allows.

If you can't do this, then even though they are clearly not  
substitutable in the example you give, in any single OWL ontology,  
there is no way to tell the difference.

I completely agree with what you say - the different semantics/models  
is/are only relevant if the query language is powerful enough to  
allow the difference to be detected; and, as you rightly point out,  
if the query language is restricted to testing the satisfiability of  
an ontology, then we can't tell the difference between (a) and (b)  
(at least not without "cheating" by using the Skolem constant in the  
query).

If, however, the query language allows me to test ontology  
entailment, then I *can* tell the difference between (a) and (b):  
given two ontologies A and B containing only axioms (a) and (b)  
respectively, then B entails A, but A doesn't entail B. This is  
because deciding if A entails B (resp. B entails A) reduces to  
deciding the satisfiability of A \cup \neg B (resp. B \cup \neg A),  
and when we introduce ontology (and hence axiom) negation, we can  
distinguish the Skolem version from the existentially quantified  
version.

Bottom line is, I suppose, that using the Skolemisation trick in  
order to avoid the use of nominals is fine provided that the kinds of  
query that will be asked will not expose the slightly stronger  
semantics.

Ian




-Alan

On Aug 17, 2006, at 1:01 AM, Ian Horrocks wrote:

On 13 Aug 2006, at 08:05, Alan Ruttenberg wrote:

This is helpful. What I am puzzling about is how I can negate the  
original axiom.

If you mean the axiom:

individual(John value(hasMother individual(value(hasMother Jane))))

then I don't believe that there is any *direct* way to negate it.  
This is pretty normal in a DL where there is typically no way to  
negate even basic Abox axioms involving roles, e.g., hasMother 
(John,Liz).

  I can see how to do it if it is written in the second form:  
"individual(John type(....".

Given that this is semantically *identical* to the first form, I  
don't see the problem of negating the axiom this way.


What I can't see is how to negate the first form - with the anonymous  
individual - and by doing so construct an OWL example that exhibits  
the difference between that and the skolemized case.

First off, I should apologise for having used hasMother in the  
example - intuitively this should be a functional property, and in  
this case the Skolemised version *is* equivalent to the existential  
version, because the mother of John *is* a unique individual. So,  
let's switch to using hasFriend. We want to show that:

individual(John value(hasFriend individual(value(hasFriend Jane))))

is *not* equivalent to

individual(John value(hasFriend individual(X value(hasFriend Jane))))

where X is a newly introduced "Skolem" individual. Note that we could  
split the second axiom into the pair of axioms

individual(John value(hasFriend X))
individual(X value(hasFriend Jane))

but a single axiom is a little easier to work with. It also makes it  
obvious that this form is strictly "stronger" than first form (it has  
fewer models, and every model of the second form is a model of the  
first, but not vice versa). As you say, we need to use the nominal  
form in order to do the negation, but I don't see why that is a  
problem. The negations turn out to be:

individual(John type(complementOf(restriction(hasFriend someValuesFrom 
(restriction(hasFriend someValuesFrom(oneOf(Jane))))))))

and

individual(John type(complementOf(restriction(hasFriend someValuesFrom 
(intersectionOf(oneOf(X) restriction(hasFriend someValuesFrom(oneOf 
(Jane)))))))))

respectively. The ontology consisting of the two axioms

individual(John value(hasFriend individual(value(hasFriend Jane))))
individual(John type(complementOf(restriction(hasFriend someValuesFrom 
(intersectionOf(oneOf(X) restriction(hasFriend someValuesFrom(oneOf 
(Jane)))))))))

is satisfiable (because there are models where the intervening friend  
is not X), but the ontology consisting of the two axioms

individual(John value(hasFriend individual(X value(hasFriend Jane))))
individual(John type(complementOf(restriction(hasFriend someValuesFrom 
(restriction(hasFriend someValuesFrom(oneOf(Jane))))))))

is not satisfiable (because the second axiom rules out Jane being a  
friend of a friend of John, regardless of the intervening individual.

I hope this covers it?

Ian




hint?

-Alan

On Aug 6, 2006, at 6:11 AM, Ian Horrocks wrote:

BTW, I've been meaning to ask you: Do I remember you once saying that  
"anonymous individuals were syntactic sugar for a nominal"? If so,  
could you explain the equivalence?

I don't remember the context. I think that what we were probably  
talking about was that the ability in OWL to describe a "chain" of  
properties linking one individual with another, e.g. (modulo syntax  
errors - this syntax drives me nuts):

individual(John value(hasMother individual(value(hasMother Jane))))

This effectively introduces an anonymous individual as the mother of  
John and daughter of Jane. We can use nominals to do this by  
asserting that John is an instance of the class of individuals whose  
mother is Jane, i.e.:

individual(John type(restriction(hasMother someValuesFrom(restriction 
(hasMother someValuesFrom(oneOf(Jane)))))))

or, in DL syntax:

John: \exists hasMother.(\exists hasMother {Jane})

The construction oneOf(Jane) defines a class whose only instance is  
Jane, i.e., the nominal {Jane}. The first existential effectively  
introduces an anonymous individual that is an instance of the class  
of individuals whose mother is Jane. We need nominals to do this,  
because they give us a way of asserting a relationship from such  
existentially quantified individuals back to named Abox individuals.

Note that a similar effect could be obtained by introducing a new  
name, e.g.,:

individual(John value(hasMother individual(newAnonInd value(hasMother  
Jane))))

or, in DL syntax:

(John, newAnonInd): hasMother
(newAnonInd, Jane): hasMother

There is a subtle difference, however, caused by "Skolemising" what  
was previously an existentially quantified individual. If we negate  
the original axiom, we get an assertion that Jane is not the  
grandmother of John, whereas if we negate the Skolemised version, we  
get an assertion that *either* newAnonInd isn't the mother of John  
*or* Jane isn't the mother of newAnonInd, i.e., Jane could still be  
the grandmother of John via some other intermediary. Depending on the  
application context, we may not notice this difference.

Ian