Protege 标记 ontology 不一致，但是 Hermit 和 Pellet Reasoner 不一致

Question

我正在尝试运行对不一致的 ontology 进行一致性检查，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;

对应的ontology是

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 将 ontology 标记为一致，而 Protege 将类标记为不一致。

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

需要car_rental is_insured_by at_most 3 credit_card; 有必要 car_rental is_insured_by at_least 5 credit_card;

对应的ontology是

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

"working fine" 你的意思是在所有三个地方你都可以看到 car_rental 是不可满足的吗？

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

minCardinality 5 和 maxCardinality 3 （在您的第二个示例中）不兼容，而是：没有数量的值可以满足两者。所以在第二个 ontology car_rental 应该是不可满足的，如果你有那个 class 的人，那么 ontology 是不一致的。

Protege 标记 ontology 不一致，但是 Hermit 和 Pellet Reasoner 不一致

Protege marks ontology inconsistent, however Hermit and Pellet Reasoner does not

owl

ontology

protege

reasoning