I am trying to run consistency check on an inconsistent ontology, for which Pellet and Hermit Reasoner is not giving an inconsistency. However Protege successfuly marks the inconsistent classes. In details, I am changing SBVR Rules to OWL 2.0. So my rules are It is necessary that car_rental is_insured_by at_least 3 credit_card; It is necessary that car_rental is_insured_by at_least 5 credit_card;
The corresponding ontology is
Prefix( xsd:=<http://www.w3.org/2001/XMLSchema#> )
Prefix( ns:=<http://isd.ktu.lt/semantika/> )
Ontology( <http://isd.ktu.lt/semantika/s2o>
Declaration( AnnotationProperty( <ns:s2o#label_sbvr> ) )
Declaration( AnnotationProperty( <ns:s2o#label_en> ) )
Declaration( Class( <ns:s2o#car_rental> ) )
AnnotationAssertion( <ns:s2o#label_sbvr> <ns:s2o#car_rental> "car_rental"@en )
AnnotationAssertion( <http://www.w3.org/2000/01/rdf-schema#label> <ns:s2o#car_rental> "car rental"@en )
AnnotationAssertion( <ns:s2o#label_en> <ns:s2o#car_rental> "car rental" )
ClassAssertion( <ns:s2o#car_rental> <ns:s2o#Car> )
Declaration( Class( <ns:s2o#credit_card> ) )
AnnotationAssertion( <ns:s2o#label_sbvr> <ns:s2o#credit_card> "credit_card"@en )
AnnotationAssertion( <http://www.w3.org/2000/01/rdf-schema#label> <ns:s2o#credit_card> "credit card"@en )
AnnotationAssertion( <ns:s2o#label_en> <ns:s2o#credit_card> "credit card" )
ClassAssertion( <ns:s2o#credit_card> <ns:s2o#Credit> )
Declaration( ObjectProperty( <ns:s2o#is_insured_by__credit_card> ) )
ObjectPropertyDomain( <ns:s2o#is_insured_by__credit_card> <ns:s2o#car_rental> )
ObjectPropertyRange( <ns:s2o#is_insured_by__credit_card> <ns:s2o#credit_card> )
AnnotationAssertion( <ns:s2o#label_sbvr> <ns:s2o#is_insured_by__credit_card> "car_rental is_insured_by credit_card"@en )
AnnotationAssertion( <http://www.w3.org/2000/01/rdf-schema#label> <ns:s2o#is_insured_by__credit_card> "car rental is insured by credit card"@en )
AnnotationAssertion( <ns:s2o#label_en> <ns:s2o#is_insured_by__credit_card> "car rental is insured by credit card" )
SubClassOf( <ns:s2o#car_rental> ObjectMinCardinality( 3 <ns:s2o#is_insured_by__credit_card> <ns:s2o#credit_card> ) )
SubClassOf( <ns:s2o#car_rental> ObjectMinCardinality( 5 <ns:s2o#is_insured_by__credit_card> <ns:s2o#credit_card> ) )
)
Hermit and Pellet marks the ontology as consistent, where as Protege marks both classes as inconsistent.
Now if I take my SBVR Rules to be as follows
It is necessary that car_rental is_insured_by at_most 3 credit_card; It is necessary that car_rental is_insured_by at_least 5 credit_card;
The corresponding ontology is
Prefix( xsd:=<http://www.w3.org/2001/XMLSchema#> )
Prefix( ns:=<http://isd.ktu.lt/semantika/> )
Ontology( <http://isd.ktu.lt/semantika/s2o>
Declaration( AnnotationProperty( <ns:s2o#label_sbvr> ) )
Declaration( AnnotationProperty( <ns:s2o#label_en> ) )
Declaration( Class( <ns:s2o#car_rental> ) )
AnnotationAssertion( <ns:s2o#label_sbvr> <ns:s2o#car_rental> "car_rental"@en )
AnnotationAssertion( <http://www.w3.org/2000/01/rdf-schema#label> <ns:s2o#car_rental> "car rental"@en )
AnnotationAssertion( <ns:s2o#label_en> <ns:s2o#car_rental> "car rental" )
ClassAssertion( <ns:s2o#car_rental> <ns:s2o#Car> )
Declaration( Class( <ns:s2o#credit_card> ) )
AnnotationAssertion( <ns:s2o#label_sbvr> <ns:s2o#credit_card> "credit_card"@en )
AnnotationAssertion( <http://www.w3.org/2000/01/rdf-schema#label> <ns:s2o#credit_card> "credit card"@en )
AnnotationAssertion( <ns:s2o#label_en> <ns:s2o#credit_card> "credit card" )
ClassAssertion( <ns:s2o#credit_card> <ns:s2o#Credit> )
Declaration( ObjectProperty( <ns:s2o#is_insured_by__credit_card> ) )
ObjectPropertyDomain( <ns:s2o#is_insured_by__credit_card> <ns:s2o#car_rental> )
ObjectPropertyRange( <ns:s2o#is_insured_by__credit_card> <ns:s2o#credit_card> )
AnnotationAssertion( <ns:s2o#label_sbvr> <ns:s2o#is_insured_by__credit_card> "car_rental is_insured_by credit_card"@en )
AnnotationAssertion( <http://www.w3.org/2000/01/rdf-schema#label> <ns:s2o#is_insured_by__credit_card> "car rental is insured by credit card"@en )
AnnotationAssertion( <ns:s2o#label_en> <ns:s2o#is_insured_by__credit_card> "car rental is insured by credit card" )
SubClassOf( <ns:s2o#car_rental> ObjectMinCardinality( 5 <ns:s2o#is_insured_by__credit_card> <ns:s2o#credit_card> ) )
SubClassOf( <ns:s2o#car_rental> ObjectMaxCardinality( 3 <ns:s2o#is_insured_by__credit_card> <ns:s2o#credit_card> ) )
)
This time Hermit and Pellet both work perfectly fine, as does Protege.
I am attaching my Hermit code as well for reference,
import java.io.File;
import java.util.Set;
import org.semanticweb.HermiT.Configuration;
import org.semanticweb.HermiT.Reasoner;
import org.semanticweb.HermiT.Reasoner.ReasonerFactory;
import org.semanticweb.owlapi.apibinding.OWLManager;
import org.semanticweb.owlapi.model.IRI;
import org.semanticweb.owlapi.model.OWLAxiom;
import org.semanticweb.owlapi.model.OWLClass;
import org.semanticweb.owlapi.model.OWLDataFactory;
import org.semanticweb.owlapi.model.OWLNamedIndividual;
import org.semanticweb.owlapi.model.OWLOntology;
import org.semanticweb.owlapi.model.OWLOntologyCreationException;
import org.semanticweb.owlapi.model.OWLOntologyManager;
import org.semanticweb.owlapi.reasoner.InconsistentOntologyException;
import org.semanticweb.owlapi.reasoner.Node;
import org.semanticweb.owlapi.reasoner.OWLReasoner;
import org.semanticweb.owlapi.reasoner.OWLReasonerFactory;
import com.clarkparsia.owlapi.explanation.BlackBoxExplanation;
import com.clarkparsia.owlapi.explanation.ExplanationGenerator;
import com.clarkparsia.owlapi.explanation.HSTExplanationGenerator;
public class Demo {
public void reason() throws OWLOntologyCreationException {
// First, we create an OWLOntologyManager object. The manager will load and save ontologies.
OWLOntologyManager m = OWLManager.createOWLOntologyManager();
OWLDataFactory dataFactory=m.getOWLDataFactory();
File inputOntologyFile = new File("C:\\Users\\1047785\\Desktop\\HermiT\\Input12.owl");
OWLOntology o=m.loadOntologyFromOntologyDocument(inputOntologyFile);// Now, we instantiate HermiT by creating an instance of the Reasoner class in the package org.semanticweb.HermiT.
Set<OWLClass> cl = o.getClassesInSignature();
//System.out.println(cl);
ReasonerFactory factory = new ReasonerFactory();
Configuration configuration=new Configuration();
configuration.throwInconsistentOntologyException = false;
OWLReasoner reasoner=factory.createReasoner(o, configuration);
BlackBoxExplanation exp=new BlackBoxExplanation(o, factory, reasoner);
HSTExplanationGenerator multExplanator=new HSTExplanationGenerator(exp);
for (OWLClass c : cl) {
System.out.println(c);
System.out.println(reasoner.isSatisfiable(c));
Set<Set<OWLAxiom>> explanations = null;
try {
explanations =multExplanator.getExplanations(c);
}
catch (Exception e) {
/*for (Set<OWLAxiom> explanation : explanations) {
System.out.println("------------------");
System.out.println("Axioms causing the unsatisfiability: ");
for (OWLAxiom causingAxiom : explanation) {
System.out.println(causingAxiom);
}
System.out.println("------------------");
}*/
continue;
}
for (Set<OWLAxiom> explanation : explanations) {
System.out.println("------------------");
System.out.println("Axioms causing the unsatisfiability: ");
for (OWLAxiom causingAxiom : explanation) {
System.out.println(causingAxiom);
}
System.out.println("------------------");
}
}
I am at a loss for this behaviour.
By "working fine" do you mean in all three places you can see car_rental as unsatisfiable?
In the first ontology, it should not be unsatisfiable: minCardinality 3 and minCardinality 5 are not incompatible restrictions: an individual with five values for the property will satisfy both.
minCardinality 5 and maxCardinality 3 (in your second example) are not compatible, instead: there is no number of values that will satisfy both. So in the second ontology car_rental should be unsatisfiable, and if you have individuals of that class the ontology is inconsistent.