Tree Paradox of OWL

classic Classic list List threaded Threaded
26 messages Options
12
Reply | Threaded
Open this post in threaded view
|

Re: Tree Paradox of OWL

Joshua TAYLOR
On Tue, May 29, 2012 at 3:15 PM, Stephan Opfer <[hidden email]> wrote:
> Thank you, for the clear examples. So the axioms must be tree shaped,
> but not their model?

I'm not sure exactly what it means to say that the axioms are tree
shaped, either, but I think it's closer.

> Although w3c states that it would break decidability to have a
> transitive and irreflexive property, there is NO proof for that! So I
> hope someone will either give that proof, or extend an OWL Reasoner to
> handle transitive and irreflexive properties.

I don't know whether there's a proof that certain combinations lead to
undecidability or not.  It's certainly the case that imposing certain
constraints, we can guarantee decidability, though.  The simple
algorithm you proposed earlier in the thread, though, would still have
some difficulties, in that certain axioms could require infinite
models and be unsatisfiable in finite models.  For instance

Integer subClassOf ( hasSuccessor some Integer )
hasSuccessor SubPropertyOf lessThan
transitive( lessThan )
irreflexive( lessThan )
zero an Integer

requires that Integer has infinitely many members which are arranged
into a tree (not necessarily a list) according to the hasSuccessor
property.  You couldn't simply walk the lessThan property, since you
wouldn't reach an end.

//JT
--
Joshua Taylor, http://www.cs.rpi.edu/~tayloj/
_______________________________________________
protege-owl mailing list
[hidden email]
https://mailman.stanford.edu/mailman/listinfo/protege-owl

Instructions for unsubscribing: http://protege.stanford.edu/doc/faq.html#01a.03
Reply | Threaded
Open this post in threaded view
|

Re: Tree Paradox of OWL

Joshua TAYLOR
On Tue, May 29, 2012 at 4:21 PM, Joshua TAYLOR <[hidden email]> wrote:

> On Tue, May 29, 2012 at 3:15 PM, Stephan Opfer <[hidden email]> wrote:
>> Thank you, for the clear examples. So the axioms must be tree shaped,
>> but not their model?
>
> I'm not sure exactly what it means to say that the axioms are tree
> shaped, either, but I think it's closer.
>
>> Although w3c states that it would break decidability to have a
>> transitive and irreflexive property, there is NO proof for that! So I
>> hope someone will either give that proof, or extend an OWL Reasoner to
>> handle transitive and irreflexive properties.
>
> I don't know whether there's a proof that certain combinations lead to
> undecidability or not.  It's certainly the case that imposing certain
> constraints, we can guarantee decidability, though.  The simple
> algorithm you proposed earlier in the thread, though, would still have
> some difficulties, in that certain axioms could require infinite
> models and be unsatisfiable in finite models.  For instance
>
> Integer subClassOf ( hasSuccessor some Integer )
> hasSuccessor SubPropertyOf lessThan
> transitive( lessThan )
> irreflexive( lessThan )
> zero an Integer
>
> requires that Integer has infinitely many members which are arranged
> into a tree (not necessarily a list) according to the hasSuccessor
> property.  You couldn't simply walk the lessThan property, since you
> wouldn't reach an end.

I'm not a DL reasoning expert by any means, and I realize that there
may have been work on the above problem (and that the standard
algorithms use blocking to handle it (or things like it?).   At any
rate, this is an interesting topic, and you might be interested in a
paper I came across while thinking about this topic (you may well have
come across it too, if you've been Googling all this while too):

Structured Objects in OWL: Representation and Reasoning
http://www.cs.ox.ac.uk/files/4557/p555-motikA.pdf

"... OWL can be used to describe domains consisting of an arbitrary or
even infinite number of objects, but it only allows for axioms that can
connect these objects in a certain tree-like manner. In other words,
OWL enjoys (a variant of) the tree model property: if an OWL ontology
has a model, then it has a model with a tree-like (or forest-like)
relational structure as well. This property is responsible for the
decidability of OWL reasoning; however, it prevents sufficiently
accurate description of complex structured objects, since schema-level
axioms in OWL cannot describe arbitrary relational  structures. ..."

--
Joshua Taylor, http://www.cs.rpi.edu/~tayloj/
_______________________________________________
protege-owl mailing list
[hidden email]
https://mailman.stanford.edu/mailman/listinfo/protege-owl

Instructions for unsubscribing: http://protege.stanford.edu/doc/faq.html#01a.03
Reply | Threaded
Open this post in threaded view
|

Re: Tree Paradox of OWL

Stephan Opfer
On 05/29/2012 10:44 PM, Joshua TAYLOR wrote:

> On Tue, May 29, 2012 at 4:21 PM, Joshua TAYLOR <[hidden email]> wrote:
>> On Tue, May 29, 2012 at 3:15 PM, Stephan Opfer <[hidden email]> wrote:
>>> Thank you, for the clear examples. So the axioms must be tree shaped,
>>> but not their model?
>>
>> I'm not sure exactly what it means to say that the axioms are tree
>> shaped, either, but I think it's closer.
>>
>>> Although w3c states that it would break decidability to have a
>>> transitive and irreflexive property, there is NO proof for that! So I
>>> hope someone will either give that proof, or extend an OWL Reasoner to
>>> handle transitive and irreflexive properties.
>>
>> I don't know whether there's a proof that certain combinations lead to
>> undecidability or not.  It's certainly the case that imposing certain
>> constraints, we can guarantee decidability, though.  The simple
>> algorithm you proposed earlier in the thread, though, would still have
>> some difficulties, in that certain axioms could require infinite
>> models and be unsatisfiable in finite models.  For instance
>>
>> Integer subClassOf ( hasSuccessor some Integer )
>> hasSuccessor SubPropertyOf lessThan
>> transitive( lessThan )
>> irreflexive( lessThan )
>> zero an Integer
>>
>> requires that Integer has infinitely many members which are arranged
>> into a tree (not necessarily a list) according to the hasSuccessor
>> property.  You couldn't simply walk the lessThan property, since you
>> wouldn't reach an end.
>
> I'm not a DL reasoning expert by any means, and I realize that there
> may have been work on the above problem (and that the standard
> algorithms use blocking to handle it (or things like it?).   At any
> rate, this is an interesting topic, and you might be interested in a
> paper I came across while thinking about this topic (you may well have
> come across it too, if you've been Googling all this while too):
>
> Structured Objects in OWL: Representation and Reasoning
> http://www.cs.ox.ac.uk/files/4557/p555-motikA.pdf
>
> "... OWL can be used to describe domains consisting of an arbitrary or
> even infinite number of objects, but it only allows for axioms that can
> connect these objects in a certain tree-like manner. In other words,
> OWL enjoys (a variant of) the tree model property: if an OWL ontology
> has a model, then it has a model with a tree-like (or forest-like)
> relational structure as well. This property is responsible for the
> decidability of OWL reasoning; however, it prevents sufficiently
> accurate description of complex structured objects, since schema-level
> axioms in OWL cannot describe arbitrary relational  structures. ..."

No didnt see that paper before, but I was just reading the description
of the tableau algorithm for SHROIQ / OWL 2:
http://www.cs.man.ac.uk/~sattler/publications/sroiq-TR.pdf

On page 23/24 the blocking is explained and I think, that your integer
example wouldn't be a problem for that blocking mechanism, because the
second and third successor of zero should have the same labels.

I will take a look into that paper you posted.

_______________________________________________
protege-owl mailing list
[hidden email]
https://mailman.stanford.edu/mailman/listinfo/protege-owl

Instructions for unsubscribing: http://protege.stanford.edu/doc/faq.html#01a.03
Reply | Threaded
Open this post in threaded view
|

Re: Tree Paradox of OWL

Thomas Schneider-2
In reply to this post by Stephan Opfer
Hi Stephan and all,

On 29.05.2012, at 21:15, Stephan Opfer wrote:

> Although w3c states that it would break decidability to have a
> transitive and irreflexive property, there is NO proof for that! So I
> hope someone will either give that proof, or extend an OWL Reasoner to
> handle transitive and irreflexive properties.

Well, it's *not* the case that, if nobody proves that transitive+irreflexive properties lead to undecidability, it is automatically straightforward to find a reasoning algorithm and write a reasoner for this extension of OWL. The examples you mentioned so far are pretty small and don't involve a lot of the remaining OWL features, and I'm pretty sure that one cannot, say, encode the domino tiling problem using *only* transitivity and irreflexivity -- which would prove undecidability. However, in the context of all OWL features, this does no longer seem obvious to me. Try to enforce a grid structure using transitivity, irreflexivity, (inverse) functionality, role chain inclusion axioms, nominals etc., and if you succeed, it's likely that you can encode a tiling.

That said, I agree that the global restrictions of OWL (which include the forbidding of declaring any composite role as irreflexive) are not "optimal" in the sense that they determine the largest fragment of "the sum of all OWL features" that is still decidable -- not even if you replace "is decidable" with "has the tree-model property". It's a highly non-trivial question of how to loosen the restrictions in the presence of all OWL features in a way that decidability is preserved. For example, Yevgeny Kazakov showed that the restriction that role chains are only allowed to occur on the left-hand side of role inclusion axioms can be loosened [1].

If you can make a good application case for an OWL *fragment* extended with irreflexivity axioms, and if you can prove that it is decidable -- usually by giving a decision procedure, ideally an implementation-friendly one --, then it is possible to get OWL reasoner developers to implement that procedure. You could also think of implementing it yourself. As for the application case, yes, I think it would be very helpful, for example, for representing mereological relations in OWL to be able to express irreflexivity. Current OWL axiomatisations are rather weak, see for example [2].

It might also be worth discussing this topic at the public-owl-dev mailing list, perhaps someone there knows more about the state of the art in terms of certain extensions of OWL (fragments).

Cheers

Thomas

[1] Yevgeny Kazakov: An Extension of Complex Role Inclusion Axioms in the Description Logic SROIQ. IJCAR 2010: 472-486. http://www.springerlink.com/content/4h47527r4x783216/?MUD=MP

[2] Thomas Bittner, Maureen Donnelly: Computational ontologies of parthood, componenthood, and containment. IJCAI 2005: 382-387. http://www.ijcai.org/papers/0829.pdf

>
> Best Regards,
>  Stephan
>
>
>
> On 05/29/2012 08:30 PM, Joshua TAYLOR wrote:
>> On Tue, May 29, 2012 at 2:03 PM, Stephan Opfer <[hidden email]> wrote:
>>> - The model of any class expression have to be tree-shaped in OWL-DL.
>>
>> A set of axioms can have non-"tree shaped models."  For instance,
>>
>> a p b;
>> a q c;
>> b r d;
>> c s d;
>>
>> is a way of satisfying the assertion that
>>
>> a is a ((p some (B and r some D)) and (q some (C and (s some D))))
>> a is an A
>> b is a B
>> c is a C
>> d is a D
>>
>> and it's "tree shaped".  What you can't do, though, is axiomatically
>> require that the p o r and the q o s chain agree on the D.
>>
>>> - There is no way to describe the fact, that individuals of one class
>>> should be connected in tree-shape, because it is impossible to forbid
>>> cycles.
>>
>> If you mean that you cannot require that the interpretation of a
>> predicate is a forest (i.e., a collection of trees), I think you're
>> right. (Though you can do *some* things that get some of the
>> properties of a forest.)
>>
>> //JT
>>
>
> _______________________________________________
> protege-owl mailing list
> [hidden email]
> https://mailman.stanford.edu/mailman/listinfo/protege-owl
>
> Instructions for unsubscribing: http://protege.stanford.edu/doc/faq.html#01a.03

----------------------------------------------------------------------
Dr. Thomas Schneider
Universität Bremen, FB 03
Postfach 330440
28334 Bremen
Germany
+49 421 218-64432
http://www.informatik.uni-bremen.de/~ts/
For visits: Cartesium, Room 2.56
----------------------------------------------------------------------

Ibstock (n.)
Anything used to make a noise on a corrugated iron wall or clinker-built fence by dragging it along the surface while walking past it. 'Mr Bennett thoughtfully selected a stout ibstock and left the house.' -- Jane Austen, Pride and Prejudice, II.

Douglas Adams, John Lloyd: The Deeper Meaning of Liff

_______________________________________________
protege-owl mailing list
[hidden email]
https://mailman.stanford.edu/mailman/listinfo/protege-owl

Instructions for unsubscribing: http://protege.stanford.edu/doc/faq.html#01a.03
Reply | Threaded
Open this post in threaded view
|

delete single individual in ontology

Katja
Hi,

I'm struggling with a problem when I updated my code to owlapi 3. I was
able to remove an individual by its name. Therefore I implemented:

public void removeIndividual(String deleteInstance) {

         OWLEntityRemover remover = new OWLEntityRemover(manager,
Collections.singleton(ontology));

         // delete all items of list

         OWLIndividual ind = getOwlIndividual(deleteInstance); //returns
the individual to be deleted
         ind.accept(remover);
         try {
             manager.applyChanges(remover.getChanges());
         } catch (OWLOntologyChangeException e) {
             // TODO Auto-generated catch block
             e.printStackTrace();
         }
         remover.reset();

     }

But now it's not working anymore. The reason is the accept() method. I
can instead remove all individuals of the ontology, but that's not what
I want.
Can someone help me out here? I guess I'm just missing a method that may
have changed or something like that.

Thanks in advance.

Cheers,
Katja

--
Dipl.-Medieninf. Katja Siegemund
Research Assistant

Technische Universität Dresden
Department of Computer Science

Phone +49 (0)40 572 44 55 1
Email [hidden email]
WWW   http://st.inf.tu-dresden.de/

_______________________________________________
protege-owl mailing list
[hidden email]
https://mailman.stanford.edu/mailman/listinfo/protege-owl

Instructions for unsubscribing: http://protege.stanford.edu/doc/faq.html#01a.03
Reply | Threaded
Open this post in threaded view
|

Re: Tree Paradox of OWL

Stephan Opfer
In reply to this post by Thomas Schneider-2
Thank you, for your comments. I just posted on the public-owl-dev
mailing list.

On 05/30/2012 11:13 AM, Thomas Schneider wrote:

> Hi Stephan and all,
>
> On 29.05.2012, at 21:15, Stephan Opfer wrote:
>
>> Although w3c states that it would break decidability to have a
>> transitive and irreflexive property, there is NO proof for that! So I
>> hope someone will either give that proof, or extend an OWL Reasoner to
>> handle transitive and irreflexive properties.
>
> Well, it's *not* the case that, if nobody proves that transitive+irreflexive properties lead to undecidability, it is automatically straightforward to find a reasoning algorithm and write a reasoner for this extension of OWL. The examples you mentioned so far are pretty small and don't involve a lot of the remaining OWL features, and I'm pretty sure that one cannot, say, encode the domino tiling problem using *only* transitivity and irreflexivity -- which would prove undecidability. However, in the context of all OWL features, this does no longer seem obvious to me. Try to enforce a grid structure using transitivity, irreflexivity, (inverse) functionality, role chain inclusion axioms, nominals etc., and if you succeed, it's likely that you can encode a tiling.
>
> That said, I agree that the global restrictions of OWL (which include the forbidding of declaring any composite role as irreflexive) are not "optimal" in the sense that they determine the largest fragment of "the sum of all OWL features" that is still decidable -- not even if you replace "is decidable" with "has the tree-model property". It's a highly non-trivial question of how to loosen the restrictions in the presence of all OWL features in a way that decidability is preserved. For example, Yevgeny Kazakov showed that the restriction that role chains are only allowed to occur on the left-hand side of role inclusion axioms can be loosened [1].
>
> If you can make a good application case for an OWL *fragment* extended with irreflexivity axioms, and if you can prove that it is decidable -- usually by giving a decision procedure, ideally an implementation-friendly one --, then it is possible to get OWL reasoner developers to implement that procedure. You could also think of implementing it yourself. As for the application case, yes, I think it would be very helpful, for example, for representing mereological relations in OWL to be able to express irreflexivity. Current OWL axiomatisations are rather weak, see for example [2].
>
> It might also be worth discussing this topic at the public-owl-dev mailing list, perhaps someone there knows more about the state of the art in terms of certain extensions of OWL (fragments).
>
> Cheers
>
> Thomas
>
> [1] Yevgeny Kazakov: An Extension of Complex Role Inclusion Axioms in the Description Logic SROIQ. IJCAR 2010: 472-486. http://www.springerlink.com/content/4h47527r4x783216/?MUD=MP
>
> [2] Thomas Bittner, Maureen Donnelly: Computational ontologies of parthood, componenthood, and containment. IJCAI 2005: 382-387. http://www.ijcai.org/papers/0829.pdf
>
>>
>> Best Regards,
>>  Stephan
>>
>>
>>
>> On 05/29/2012 08:30 PM, Joshua TAYLOR wrote:
>>> On Tue, May 29, 2012 at 2:03 PM, Stephan Opfer <[hidden email]> wrote:
>>>> - The model of any class expression have to be tree-shaped in OWL-DL.
>>>
>>> A set of axioms can have non-"tree shaped models."  For instance,
>>>
>>> a p b;
>>> a q c;
>>> b r d;
>>> c s d;
>>>
>>> is a way of satisfying the assertion that
>>>
>>> a is a ((p some (B and r some D)) and (q some (C and (s some D))))
>>> a is an A
>>> b is a B
>>> c is a C
>>> d is a D
>>>
>>> and it's "tree shaped".  What you can't do, though, is axiomatically
>>> require that the p o r and the q o s chain agree on the D.
>>>
>>>> - There is no way to describe the fact, that individuals of one class
>>>> should be connected in tree-shape, because it is impossible to forbid
>>>> cycles.
>>>
>>> If you mean that you cannot require that the interpretation of a
>>> predicate is a forest (i.e., a collection of trees), I think you're
>>> right. (Though you can do *some* things that get some of the
>>> properties of a forest.)
>>>
>>> //JT
>>>
>>
>> _______________________________________________
>> protege-owl mailing list
>> [hidden email]
>> https://mailman.stanford.edu/mailman/listinfo/protege-owl
>>
>> Instructions for unsubscribing: http://protege.stanford.edu/doc/faq.html#01a.03
>
> ----------------------------------------------------------------------
> Dr. Thomas Schneider
> Universität Bremen, FB 03
> Postfach 330440
> 28334 Bremen
> Germany
> +49 421 218-64432
> http://www.informatik.uni-bremen.de/~ts/
> For visits: Cartesium, Room 2.56
> ----------------------------------------------------------------------
>
> Ibstock (n.)
> Anything used to make a noise on a corrugated iron wall or clinker-built fence by dragging it along the surface while walking past it. 'Mr Bennett thoughtfully selected a stout ibstock and left the house.' -- Jane Austen, Pride and Prejudice, II.
>
> Douglas Adams, John Lloyd: The Deeper Meaning of Liff
>
> _______________________________________________
> protege-owl mailing list
> [hidden email]
> https://mailman.stanford.edu/mailman/listinfo/protege-owl
>
> Instructions for unsubscribing: http://protege.stanford.edu/doc/faq.html#01a.03
>

_______________________________________________
protege-owl mailing list
[hidden email]
https://mailman.stanford.edu/mailman/listinfo/protege-owl

Instructions for unsubscribing: http://protege.stanford.edu/doc/faq.html#01a.03
12