Questions about Unsatisfiability explanations in protégé

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

Questions about Unsatisfiability explanations in protégé

OntoBLW
Hello,
*First problem:*
I want to add this axiom: SubClassOf(:clss3 ObjectMinCardinality(2 :prop1
clss5))
Given a part of my ontology:

1)DisjointClasses(:E :clss5)
2)ObjectPropertyRange(:prop1 :E)
3)SubClassOf(:clss3 ObjectMaxCardinality(5 :prop1))

I tried to test (in may program) that DisjointClasses(ObjectMaxCardinality(5
:prop1)  ObjectMinCardinality(2 :prop1 :clss5) and I intuitively know that
they are not. However, the reasoner entails this disjointness: When I
requested the explanation plugin to explain such entailment, it gives me
this explanation:

DisjointClasses(:E :clss5)
ObjectPropertyRange(:prop1 :E)
 Yet I have not understood how these two axioms entail the disjointness. I
know that these two axioms (1 and 2) are contradictory with
SubClassOf(:clss3 ObjectMinCardinality(2 :prop1 clss5)) *but I don't
understand why/how they entail DisjointClasses(ObjectMaxCardinality(5
:prop1)  ObjectMinCardinality(2 :prop1 :clss5).*
 Thank you for explaining me this issue.

*Second problem:*
I tried to change the cardinality of the axiom 3 as follows
SubClassOf(:clss3 ObjectMaxCardinality(1 :prop1)) and I tried to test the
disjointness DisjointClasses(ObjectMaxCardinality(5 :prop1)
ObjectMinCardinality(2 :prop1 :clss5). Intuitively, the disjointness here is
obvious (not as the first case). Then, I tried to request an explanation for
this disjointness. However, the explanation plugin was generating more than
3500 explanations(non stopping).
Could you please explain this no stopping explanation?

Thank you in advance for your answers.



--
Sent from: http://protege-project.136.n4.nabble.com/Protege-Developer-f4659816.html
_______________________________________________
protege-dev mailing list
[hidden email]
https://mailman.stanford.edu/mailman/listinfo/protege-dev
Reply | Threaded
Open this post in threaded view
|

Re: Questions about Unsatisfiability explanations in protégé

Csongor Nyulas
Administrator
Hi,

The key to both of your problem is that the class ObjectMinCardinality(2 :prop1 :clss5) is unsatisfiable, i.e. it is the subclass of owl:Nothing, or in other words it is the empty set.
The explanation for this is that the range of property :prop1 is :E (conform axiom 2), which means that everything that :prop1 relates to, is an instance of :E, however we know from axiom 1 that :E and :clss5 do not share any instances (they are disjoint). So there cannot exists any individual in the world that would have a relation :prop1 to an instance of the class :clss5, and if it can't have one such relation, it can't have 2 either.



So, if ObjectMinCardinality(2 :prop1 :clss5) is the empty set, then it is a subclass of every other class. Therefore, it is not disjoint with ObjectMaxCardinality(5 :prop1) (as you intuitively knew), but rather a subclass of it,  as it is subclass of :E, :clss5, :clss3, ObjectMaxCardinality(1 :prop1), etc.

If you make SubClassOf(:clss3 ObjectMinCardinality(2 :prop1,clss5)), :clss3 will become unsatisfiable as well.

I attach an ontology that demonstrates this. I have created defined classes testMax5Thing and testMin2C5 which are equivalent to ObjectMinCardinality(2 :prop1 :clss5) and ObjectMinCardinality(2 :prop1 :clss5) respectively, to better illustrate what is happening.




Csongor


On 11/07/2017 08:42 AM, OntoBLW wrote:
Hello,
*First problem:*
I want to add this axiom: SubClassOf(:clss3 ObjectMinCardinality(2 :prop1
clss5))
Given a part of my ontology:

1)DisjointClasses(:E :clss5)
2)ObjectPropertyRange(:prop1 :E)
3)SubClassOf(:clss3 ObjectMaxCardinality(5 :prop1))

I tried to test (in may program) that DisjointClasses(ObjectMaxCardinality(5
:prop1)  ObjectMinCardinality(2 :prop1 :clss5) and I intuitively know that
they are not. However, the reasoner entails this disjointness: When I
requested the explanation plugin to explain such entailment, it gives me
this explanation:

DisjointClasses(:E :clss5)
ObjectPropertyRange(:prop1 :E)
 Yet I have not understood how these two axioms entail the disjointness. I
know that these two axioms (1 and 2) are contradictory with
SubClassOf(:clss3 ObjectMinCardinality(2 :prop1 clss5)) *but I don't
understand why/how they entail DisjointClasses(ObjectMaxCardinality(5
:prop1)  ObjectMinCardinality(2 :prop1 :clss5).*
 Thank you for explaining me this issue.

*Second problem:*
I tried to change the cardinality of the axiom 3 as follows
SubClassOf(:clss3 ObjectMaxCardinality(1 :prop1)) and I tried to test the
disjointness DisjointClasses(ObjectMaxCardinality(5 :prop1) 
ObjectMinCardinality(2 :prop1 :clss5). Intuitively, the disjointness here is
obvious (not as the first case). Then, I tried to request an explanation for
this disjointness. However, the explanation plugin was generating more than
3500 explanations(non stopping).
Could you please explain this no stopping explanation?

Thank you in advance for your answers.



--
Sent from: http://protege-project.136.n4.nabble.com/Protege-Developer-f4659816.html
_______________________________________________
protege-dev mailing list
[hidden email]
https://mailman.stanford.edu/mailman/listinfo/protege-dev


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

cardRestrTest.owl (1K) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Questions about Unsatisfiability explanations in protégé

OntoBLW
Hi,
Thank you for your answer. Yes, it's correct that ObjectMinCardinality(2
:prop1 :clss5) is not disjoint with ObjectMaxCardinality(5 :prop1), but why
did I find that the reasoner entails that disjointness (in both cases: the
second case is obvious but the first is not)?
Note:SubClassOf(clss3 ObjectMinCardinality(2 :prop1 :clss5)) is not added
yet when I test this disjointness.



--
Sent from: http://protege-project.136.n4.nabble.com/Protege-Developer-f4659816.html
_______________________________________________
protege-dev mailing list
[hidden email]
https://mailman.stanford.edu/mailman/listinfo/protege-dev
Reply | Threaded
Open this post in threaded view
|

Re: Questions about Unsatisfiability explanations in protégé

Csongor Nyulas
Administrator
You must be interpreting something wrong. How do you test for disjointness?

If I look at the result of the inference in Protege (after running HermiT), testMin2C5 (which is equivalent to ObjectMinCardinality(2 :prop1 :clss5) ) is NOT disjoint with testMax5Thing (representing ObjectMaxCardinality(5 :prop1)). See below...



On the contrary, if I look at the subclasses of testMax5Thing I do see testMin2C5 listed there. So, no, testMax5Thing and testMin2C5 are not disjoint.



Csongor



On 11/07/2017 01:25 PM, OntoBLW wrote:
Hi,
Thank you for your answer. Yes, it's correct that ObjectMinCardinality(2
:prop1 :clss5) is not disjoint with ObjectMaxCardinality(5 :prop1), but why
did I find that the reasoner entails that disjointness (in both cases: the
second case is obvious but the first is not)?
Note:SubClassOf(clss3 ObjectMinCardinality(2 :prop1 :clss5)) is not added
yet when I test this disjointness.



--
Sent from: http://protege-project.136.n4.nabble.com/Protege-Developer-f4659816.html
_______________________________________________
protege-dev mailing list
[hidden email]
https://mailman.stanford.edu/mailman/listinfo/protege-dev


_______________________________________________
protege-dev mailing list
[hidden email]
https://mailman.stanford.edu/mailman/listinfo/protege-dev
Reply | Threaded
Open this post in threaded view
|

Re: Questions about Unsatisfiability explanations in protégé

OntoBLW
Hi again,
Here is how I tested the disjointness:
 } else if
((((superClassI.getClassExpressionType().equals(ClassExpressionType.OBJECT_EXACT_CARDINALITY)))
||
(((superClassI.getClassExpressionType().equals(ClassExpressionType.OBJECT_MAX_CARDINALITY)))))
&& (((OWLObjectCardinalityRestriction)
superClassI).getProperty().equals(objProperty))) {
                           
if(reasoner.isEntailed(modelManager.getOWLDataFactory().getOWLDisjointClassesAxiom(superClassI,
(OWLObjectMinCardinality) superClass))) {
                                potentialInconsistency=true;
                                System.out.println("result of disjointness
test
"+reasoner.isEntailed(modelManager.getOWLDataFactory().getOWLDisjointClassesAxiom(superClassI,
(OWLObjectMinCardinality) superClass)));
                               
if(modelManager.getExplanationManager().hasExplanation(modelManager.getOWLDataFactory().getOWLDisjointClassesAxiom(superClassI,
(OWLObjectMinCardinality) superClass))) {
                   
modelManager.getExplanationManager().handleExplain((Frame)
SwingUtilities.getAncestorOfClass(Frame.class, this),
modelManager.getOWLDataFactory().getOWLDisjointClassesAxiom(superClassI,
(OWLObjectMinCardinality) superClass));

                }

The log displays:

<http://protege-project.136.n4.nabble.com/file/t375701/2017-11-08_10-24-45.png>

the explanation plugin displays:

<http://protege-project.136.n4.nabble.com/file/t375701/java_2017-11-08_10-26-24.png>

Thank you again for your interest and explaining me the problem.



--
Sent from: http://protege-project.136.n4.nabble.com/Protege-Developer-f4659816.html
_______________________________________________
protege-dev mailing list
[hidden email]
https://mailman.stanford.edu/mailman/listinfo/protege-dev