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://protegeproject.136.n4.nabble.com/ProtegeDeveloperf4659816.html _______________________________________________ protegedev mailing list [hidden email] https://mailman.stanford.edu/mailman/listinfo/protegedev 
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://protegeproject.136.n4.nabble.com/ProtegeDeveloperf4659816.html _______________________________________________ protegedev mailing list [hidden email] https://mailman.stanford.edu/mailman/listinfo/protegedev _______________________________________________ protegedev mailing list [hidden email] https://mailman.stanford.edu/mailman/listinfo/protegedev cardRestrTest.owl (1K) Download Attachment 
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://protegeproject.136.n4.nabble.com/ProtegeDeveloperf4659816.html _______________________________________________ protegedev mailing list [hidden email] https://mailman.stanford.edu/mailman/listinfo/protegedev 
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://protegeproject.136.n4.nabble.com/ProtegeDeveloperf4659816.html _______________________________________________ protegedev mailing list [hidden email] https://mailman.stanford.edu/mailman/listinfo/protegedev _______________________________________________ protegedev mailing list [hidden email] https://mailman.stanford.edu/mailman/listinfo/protegedev 
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://protegeproject.136.n4.nabble.com/file/t375701/20171108_102445.png> the explanation plugin displays: <http://protegeproject.136.n4.nabble.com/file/t375701/java_20171108_102624.png> Thank you again for your interest and explaining me the problem.  Sent from: http://protegeproject.136.n4.nabble.com/ProtegeDeveloperf4659816.html _______________________________________________ protegedev mailing list [hidden email] https://mailman.stanford.edu/mailman/listinfo/protegedev 
Free forum by Nabble  Edit this page 