Protege отмечает, что онтология несовместима, однако Отшельник и Пелле 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>)) 
) 

Отшельника и пеллеты отмечают онтологию как последовательные, где, как 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>)) 
) 

На этот раз Отшельник и пеллетах оба работают прекрасно, как это делает 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 должно быть неудовлетворительным, и если у вас есть люди этого класса, онтология несовместима.