OWL : Does disjoint "general class axiom" via a property only works if classes themselves are disjointed?
For example 1 :
- Classes : A and B.
- Property : hasValue.
- Axiom : hasValue some A disjointWith hasValue some B.
- Individual : user1.
- user1 hasValue A.
- user1 hasValue B.
Protege reasoner (HermiT) throws no error.
For example 2 :
- Classes : A and B.
- A disjoint with B.
- Property : hasValue.
- Axiom : hasValue some A disjointWith hasValue some B.
- Individual : user1.
- user1 hasValue A.
- user1 hasValue B.
Protege reasoner (HermiT) throws error.
Shouldn't "hasValue some A disjointWith hasValue some B" alone be sufficient to throw error in eg 1's case?
EDIT : example 1's reasoner result is wrong. As @Henriette Harmse showed below reasoner will throw error.
I was doing declaring Axiom a little differently than what I wrote above. I declared axiom as "hasValue some B DisjointWith hasValue some (P and (not (B)))", where P is parent class of both A and B. (Full sample ontology below.) If you import it in protege and run, you'll not get error.
It seems :
- "hasValue some B DisjointWith hasValue some A"
- "hasValue some B DisjointWith hasValue some (P and (not (B)))"
are not equivalent statements.
Sample ontology :
@prefix : <http://test.org/#> .
@prefix owl: <http://www.w3.org/2002/07/owl#> .
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix xml: <http://www.w3.org/XML/1998/namespace> .
@prefix xsd: <http://www.w3.org/2001/XMLSchema#> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
@base <http://test.org/> .
<http://test.org/> rdf:type owl:Ontology .
#################################################################
# Object Properties
#################################################################
### http://test.org/#hasValue
:hasValue rdf:type owl:ObjectProperty .
#################################################################
# Classes
#################################################################
### http://test.org/#A
:A rdf:type owl:Class ;
rdfs:subClassOf :P .
### http://test.org/#B
:B rdf:type owl:Class ;
rdfs:subClassOf :P .
### http://test.org/#P
:P rdf:type owl:Class .
### http://test.org/#USER
:USER rdf:type owl:Class .
#################################################################
# Individuals
#################################################################
### http://test.org/#A
:A rdf:type owl:NamedIndividual ,
:A .
### http://test.org/#B
:B rdf:type owl:NamedIndividual ,
:B .
### http://test.org/#user1
:user1 rdf:type owl:NamedIndividual ;
:hasValue :A ,
:B .
#################################################################
# General axioms
#################################################################
[ rdf:type owl:Restriction ;
owl:onProperty :hasValue ;
owl:someValuesFrom :A ;
owl:disjointWith [ rdf:type owl:Restriction ;
owl:onProperty :hasValue ;
owl:someValuesFrom [ owl:intersectionOf ( :P
[ rdf:type owl:Class ;
owl:complementOf :A
]
) ;
rdf:type owl:Class
]
]
] .
[ rdf:type owl:Restriction ;
owl:onProperty :hasValue ;
owl:someValuesFrom :B ;
owl:disjointWith [ rdf:type owl:Restriction ;
owl:onProperty :hasValue ;
owl:someValuesFrom [ owl:intersectionOf ( :P
[ rdf:type owl:Class ;
owl:complementOf :B
]
) ;
rdf:type owl:Class
]
]
] .
### Generated by the OWL API (version 4.5.9.2019-02-01T07:24:44Z) https://github.com/owlcs/owlapi
I have tried this now myself and for your first example I get an inconsistency with the following explanation:
Here is the actual ontology giving the inconsistency. I will need to see your actual ontology to understand why you are not getting an inconsistency.
<?xml version="1.0"?>
<rdf:RDF xmlns="http://www.semanticweb.org/henri/ontologies/2022/6/untitled-ontology-9#"
xml:base="http://www.semanticweb.org/henri/ontologies/2022/6/untitled-ontology-9"
xmlns:owl="http://www.w3.org/2002/07/owl#"
xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
xmlns:xml="http://www.w3.org/XML/1998/namespace"
xmlns:xsd="http://www.w3.org/2001/XMLSchema#"
xmlns:rdfs="http://www.w3.org/2000/01/rdf-schema#"
xmlns:untitled-ontology-9="http://www.semanticweb.org/henri/ontologies/2022/6/untitled-ontology-9#">
<owl:Ontology rdf:about="http://www.semanticweb.org/henri/ontologies/2022/6/untitled-ontology-9"/>
<owl:ObjectProperty rdf:about="http://www.semanticweb.org/henri/ontologies/2022/6/untitled-ontology-9#hasValue"/>
<owl:Class rdf:about="http://www.semanticweb.org/henri/ontologies/2022/6/untitled-ontology-9#A"/>
<owl:Class rdf:about="http://www.semanticweb.org/henri/ontologies/2022/6/untitled-ontology-9#B"/>
<owl:NamedIndividual rdf:about="http://www.semanticweb.org/henri/ontologies/2022/6/untitled-ontology-9#a">
<rdf:type rdf:resource="http://www.semanticweb.org/henri/ontologies/2022/6/untitled-ontology-9#A"/>
</owl:NamedIndividual>
<owl:NamedIndividual rdf:about="http://www.semanticweb.org/henri/ontologies/2022/6/untitled-ontology-9#b">
<rdf:type rdf:resource="http://www.semanticweb.org/henri/ontologies/2022/6/untitled-ontology-9#B"/>
</owl:NamedIndividual>
<owl:NamedIndividual rdf:about="http://www.semanticweb.org/henri/ontologies/2022/6/untitled-ontology-9#user1">
<hasValue rdf:resource="http://www.semanticweb.org/henri/ontologies/2022/6/untitled-ontology-9#a"/>
<hasValue rdf:resource="http://www.semanticweb.org/henri/ontologies/2022/6/untitled-ontology-9#b"/>
</owl:NamedIndividual>
<owl:Restriction>
<owl:onProperty rdf:resource="http://www.semanticweb.org/henri/ontologies/2022/6/untitled-ontology-9#hasValue"/>
<owl:someValuesFrom rdf:resource="http://www.semanticweb.org/henri/ontologies/2022/6/untitled-ontology-9#A"/>
<owl:disjointWith>
<owl:Restriction>
<owl:onProperty rdf:resource="http://www.semanticweb.org/henri/ontologies/2022/6/untitled-ontology-9#hasValue"/>
<owl:someValuesFrom rdf:resource="http://www.semanticweb.org/henri/ontologies/2022/6/untitled-ontology-9#B"/>
</owl:Restriction>
</owl:disjointWith>
</owl:Restriction>
</rdf:RDF>
Update after reviewing ACTUAL ontology
The main problem is that you stated the GCI you used incorrectly. What you said you used are substantially different from what you actually used.
What you said used: hasValue some A disjointWith hasValue some B
What you actually used:
hasValue some A DisjointWith hasValue some (P and (not (A)))
hasValue some B DisjointWith hasValue some (P and (not (B)))
To understand why your GCIs do not have the desired effect, I have drawn an example Venn diagram:
Note that hasValue some A DisjointWith hasValue some (P and (not (A))) states that there is no individual x that belongs to both the set hasValue some A and the set hasValue some (P and (not (A))). It does however allow for the possibility that you have an individual user1 that is related via hasValue to an individual in set A and that is related via hasValue to an individual in set B. This is because nothing prohibits the sets hasValue some A (to which user1 hasValue A belongs) and hasValue some B (to which user1 hasValue B belongs)` to overlap. To prohibit this, you have to add the following GCI:
hasValue some A DisjointWith hasValue some B
How to get a inconsistency using you GCIs
To get an inconsistency using your GCIs, you have to have an individual that actually belong to the disjoint sets you defined. I.e.,
Define individual x as follows:
:x rdf:type owl:NamedIndividual ,
[ owl:intersectionOf ( :P
[ rdf:type owl:Class ;
owl:complementOf :A
]
) ;
rdf:type owl:Class
] .
and then define user2:
:user2 rdf:type owl:NamedIndividual ;
:hasValue :A ,
:x .
You will get an inconsistency with the following explanation:
