OWL 2 ontology consistency check

Question

I am trying to change SBVR Rules to Ontologies(OWL 2) and then running a consistency check on them using Hermit Reasoner. However even in case of inconsistent rules and thus inconsistent ontologies, the Hermit Reasoner is showing the ontology to be consistent. I am at a loss at where I am going wrong.

The ontology(OWL 2) I got is as follows:

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#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" )
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" )
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> ObjectMaxCardinality( 2 <ns:s2o#is_insured_by__credit_card> <ns:s2o#credit_card> ) )
)

The corresponding SBVR rules and vocabulary is as follows:

Vocabulary

credit_card

car_rental

car_rental is_insured_by credit_card

Rules

It is necessary that car_rental is_insured_by at_least 3 credit_card;

It is necessary that car_rental is_insured_by at_most 2 credit_card;

The SBVR rules are clearly contrasting and so inconsistent. I would like to know whether the Ontology is inconsistent as well, and if so why is the reasoner not working. It looks to me it is, but I am at a loss as to why the Hermit Reasoner is saying otherwise.

I have added Hermit.jar to my java code and running reasoner on it.

The code for that is

    package com.tcs.HermiT;

import java.io.File;

import org.semanticweb.HermiT.Reasoner;
import org.semanticweb.owlapi.apibinding.OWLManager;
import org.semanticweb.owlapi.model.IRI;
import org.semanticweb.owlapi.model.OWLOntology;
import org.semanticweb.owlapi.model.OWLOntologyManager;

public class Demo {

    public static void main(String[] args) throws Exception {
        // First, we create an OWLOntologyManager object. The manager will load and save ontologies.
        OWLOntologyManager m = OWLManager.createOWLOntologyManager();
        // We use the OWL API to load the Pizza ontology.
        File inputOntologyFile = new File("C:\\Users\\1047785\\Desktop\\HermiT\\Input9.owl");
        OWLOntology o=m.loadOntologyFromOntologyDocument(inputOntologyFile);// Now, we instantiate HermiT by creating an instance of the Reasoner class in the package org.semanticweb.HermiT.
        Reasoner hermit=new Reasoner(o);
        //System.out.println(hermit.getDLOntology());
        // Finally, we output whether the ontology is consistent.
        System.out.println(hermit.isConsistent());
        //System.out.println(hermit.getDLOntology().toString());

    }
}

Answer 1

The ontology as presented is not inconsistent. The contradicting cardinality restrictions leads to the unsatisfiability of class car_rental. HermiT correctly detects this, and Protege shows this marking that class in red and classifying it as a subclass of Nothing. However, as long as this class contains no instances, the ontology stays consistent.In order to make it inconsistent due to those contradictory restrictions, you must have at least one instance of that class.