使用 Pellet 推理器的 Java 中 OWL 本体的不一致性和可满足性

Question

我正在尝试查看本体是否一致。 本体可以是一致的，但仍然可能有一些无法满足的类。我们称之为案例A。

但我的问题是，当本体无法通过一致性测试时，即不一致（Case B）。我的问题是即使在案例 B 中我也无法获得无法满足的本体类。

我的最终目标是处理不可满足的类以对其进行一些更改，并将不一致的本体变为一致的本体。因此，我可以在 Case A 中实现我的目标（我可以访问无法满足的类），我会处理它们并修改其中的一些。但是，现在，我能为案例 B 做些什么呢？

下面的代码展示了这两种情况。

   OWLReasonerFactory reasonerFactory = new PelletReasonerFactory();
   OWLReasoner reasoner = reasonerFactory.createNonBufferingReasoner(myOntology);

    if (reasoner.isConsistent()) {
        if (reasoner.getUnsatisfiableClasses().getEntitiesMinusBottom().size() > 0) {
            System.out.println("ontology is consistent but has unsatisfiable classes! FAILED");
                    // CASE A
        } else {
            System.out.println("ontology is consistent and safe without any unsatisfiable classes! PASSED");
        }

    } else {
        System.out.println("ontology is inconsistent!FAILED");
                // CASE B
    }

对于案例 B，我能做什么？ 在here，它写道：

如果要查找不可满足的类，只需对所有类调用 isSatisfiable 方法即可： reasoner.isSatisfiable(className);

我在案例B中加入了以下代码：

    Iterator<OWLClass> cAll = myOntology.getClassesInSignature().iterator();
    while (cAll.hasNext()) {
            OWLClass c = cAll.next();
            if (!reasoner.isSatisfiable(c)) {
                System.out.println("class " + c + "is not satisfibale");
            }
    }

但我得到一个错误，如：

Exception in thread "main" org.semanticweb.owlapi.reasoner.InconsistentOntologyException: Inconsistent ontology
    at com.clarkparsia.pellet.owlapiv3.PelletReasoner.convert(PelletReasoner.java:360)
    at com.clarkparsia.pellet.owlapiv3.PelletReasoner.isSatisfiable(PelletReasoner.java:890)

那么如何处理案例B中的本体呢？

更新

基于@Ignazio 的cmets，在我的问题代码中，在 //CASE B 的位置，我调用了这个新函数：

public static void run(OWLOntology myOnt) {
    // save the Tbox and Abox of the original ontology
    Set<OWLAxiom> originalTboxAxioms = myOnt.getTBoxAxioms(true);
    Set<OWLAxiom> originalAboxAxioms = myOnt.getABoxAxioms(true);

    // create new empty ontology
    String name = "local_path//name.owl";
    OWLOntologyManager manager = OWLManager.createOWLOntologyManager();
    File fileM = new File(name);
    OWLOntology newOntology = null;

    try {
        newOntology = manager.createOntology(IRI.create(fileM));
    } catch (OWLOntologyCreationException e) {
        e.printStackTrace();
    }

    // add only Tboxes from the orginal ontology to the new one
    manager.addAxioms(newOntology, originalTboxAxioms);

    // checking the consistency of the new ontology which contain only tbox
    OWLReasonerFactory reasonerFactory = new PelletReasonerFactory();
    Configuration configuration = new Configuration();
    configuration.throwInconsistentOntologyException = false;
    OWLReasoner reasoner = reasonerFactory.createNonBufferingReasoner(newOntology, configuration);

    if (reasoner.isConsistent()) {
       Set<OWLClass> unSat = reasoner.getUnsatisfiableClasses().getEntitiesMinusBottom();        
       if (unSat.size() > 0) {
            Iterator<OWLClass> unClassList = unSat.iterator();

            Set<OWLClass> listOfUnsatisfiableClasses = new HashSet<OWLClass>();
            while (unClassList.hasNext()) {
                /*
                 * if the unsatisfiable class appear in the original Abox,
                 * we mark it as an unsatisfiable class
                 */
                OWLClass myClass = unClassList.next();
                Iterator<OWLAxiom> iter = originalAboxAxioms.iterator();
                    while (iter.hasNext()){
                        OWLAxiom ax = iter.next();
                        if (ax.getClassesInSignature().contains(myClass)){
                            listOfUnsatisfiableClasses.add(myClass);    
                        }
                    }
            }
            System.out.println("number of unsatisfiable classes: " + listOfUnsatisfiableClasses.size());
        }
    }
    System.out.println("The ontology is inconsistent but does not have any unsatisfiable classes!!!!!");
}

即使有了这个新功能，也找不到不满意的课程！

我还尝试了@Ignazio 发布的here 中的代码。对于那里给定的示例，该代码将在几秒钟内运行，但对于我小的不一致本体，即使在 1 天后，也不会打印任何结果。

您知道如何将不可满足的类连同它们的理由集一起获得吗？

Answer 1

不一致的本体意味着存在无法满足的类的实例，或者存在两个或多个被声明为不相交的类的实例。

（可能有些人被声明为 owl:Nothing 类型，但这很容易检测到并且可能是一个错误。）

要确定不一致是否取决于不可满足的类，您可以尝试将 abox 和 tbox 分开 - 然后单独检查 tbox。您可以使用 AxiomType 中的便捷方法列出属于 tbox 的公理类型。

更新：查看代码，有几处需要修复：

    if (reasoner.getUnsatisfiableClasses().getEntitiesMinusBottom().size() > 0) {
        ^^^^^^^^^^^^^^ you're calling reasoner.getUnsatisfiableClasses() twice,
                       forcing the reasoner to do more work than necessary.
                       Store this set in a local variable, or skip the size check
                       (if the set is empty, the iterator will be empty
                       and you'll skip the while anyway.
      Iterator<OWLClass> unClassList = reasoner.getUnsatisfiableClasses().getEntitiesMinusBottom().iterator();


        Set<OWLClass> listOfUnsatisfiableClasses = new HashSet<OWLClass>();
        while (unClassList.hasNext()) {
            /*
             * if the unsatisfiable class appear in the original Abox,
             * we mark it as an unsatisfiable class
             */
            OWLClass myClass = unClassList.next();
            if (originalAboxAxioms.contains(myClass))
                listOfUnsatisfiableClasses.add(myClass);
            ^^^^^^ this code is not doing what the comment is saying.
                   originalAboxAxioms contains abox axioms, not classes,
                   so you'll never get true as a result of this lookup.
                   Also, the classes will necessarily be part of the ontology,
                   so you can skip this altogether.
        }
        System.out.println("number of unsatisfiable classes: " + listOfUnsatisfiableClasses.size());
    }