OWL 2 本体一致性检查

Question

我正在尝试将 SBVR 规则更改为 Ontologies(OWL 2)，然后使用 Hermit Reasoner 对它们进行一致性检查。然而，即使在规则不一致从而本体不一致的情况下，隐士推理者也显示本体是一致的。我不知道哪里出错了。

我得到的本体（OWL 2）如下：

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> ) )
)

对应的SBVR规则和词汇如下：

词汇

信用卡

汽车租赁

car_rental is_insured_by credit_card

规则

car_rental is_insured_by at_least 3 credit_card 是必要的；

car_rental 需要最多 2 张信用卡投保；

SBVR 规则明显对比，因此不一致。我想知道本体是否也不一致，如果是，为什么推理器不起作用。在我看来确实如此，但我不知道为什么隐士推理者会这么说。

我已将 Hermit.jar 添加到我的 java 代码中并在其上运行推理器。

代码是

    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

呈现的本体并不矛盾。矛盾的基数限制导致类car_rental 的不可满足性。 HermiT 正确地检测到了这一点，Protege 将这个类标记为红色并将其分类为Nothing 的子类。但是，只要该类不包含实例，本体就保持一致。为了使其由于这些矛盾的限制而不一致，您必须至少具有该类的一个实例。