Protege 标记本体不一致，但 Hermit 和 Pellet Reasoner 没有

Question

我正在尝试对不一致的本体运行一致性检查，而 Pellet 和 Hermit Reasoner 并没有给出不一致的结果。然而，Protege 成功地标记了不一致的类。 具体来说，我将 SBVR 规则更改为 OWL 2.0。 所以我的规则是 car_rental is_insured_by at_least 3 credit_card 是必要的； car_rental is_insured_by at_least 5 credit_card 是必要的；

对应的本体是

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 和 Pellet 将本体标记为一致，而 Protege 将两个类标记为不一致。

现在，如果我将我的 SBVR 规则如下

car_rental is_insured_by at_most 3 credit_card 是必要的； car_rental is_insured_by at_least 5 credit_card 是必要的；

对应的本体是

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

这一次 Hermit 和 Pellet 都可以正常工作，Protege 也是如此。

我也附上我的隐士代码以供参考，

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("------------------");
            }

        }

我对这种行为不知所措。

Answer 1

你所说的“工作正常”是指在所有三个地方你都认为car_rental 不能令人满意吗？

在第一个本体中，它不应该是不可满足的：minCardinality 3 和 minCardinality 5 不是不兼容的限制：具有五个属性值的个体将同时满足两者。

minCardinality 5 和 maxCardinality 3 （在您的第二个示例中）不兼容，而是：没有多少值可以同时满足两者。所以在第二个本体car_rental 应该是不能满足的，如果你有那个类的个体，本体是不一致的。