Discussion of anonymous individuals versus 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
>>>>
>>>
>>
>