OWLAPI与HermiT推理器问题：已删除个体仍被推断为owl:Thing实例

我在结合使用OWLAPI与HermiT推理器时遇到一个问题：删除个体后，该个体仍被判定为owl:Thing的实例，导致单元测试失败。

问题重现测试代码 #

boolean added = ontology.addIndividualToClass("Person", login);
Assert.isTrue(added, "The individual must be present.");
ontology.think();

boolean exists = ontology.doesIndividualBelongToClass("Person", login);
Assert.isTrue(exists, "The individual must be found.");

boolean removed = ontology.removeIndividualFromClass("Person", login);
Assert.isTrue(removed, "The individual must be removed.");
ontology.think();

// 此断言正常通过
exists = ontology.doesIndividualBelongToClass("Person", login);
Assert.isTrue(!exists, "The individual must not be found.");

// 此断言触发失败
exists = ontology.doesIndividualExist(login);
Assert.isTrue(!exists, "The individual must not be present.");

核心方法逻辑 #

• 添加方法：生成目标类的类断言并添加到本体
• 删除方法：查找并移除对应个体的目标类断言
• 检测方法：同时校验推理器推断的个体和本体中声明的个体归属关系

相关方法实现 #

添加个体到类的方法 #

public boolean addIndividualToClass(String className, String login) {
    [...]  // 参数校验
    OWLNamedIndividual individual = dataFactory.getOWLNamedIndividual(individualName, prefixManager);
    if (individual == null) throw new IllegalArgumentException("Could not get named individual.");
    OWLClassAssertionAxiom classAssertion = dataFactory.getOWLClassAssertionAxiom(clazz, individual);
    ChangeApplied changed = ontology.add(classAssertion);
    return changed.equals(ChangeApplied.SUCCESSFULLY) || changed.equals(ChangeApplied.NO_OPERATION);
}

从类中删除个体的方法 #

public boolean removeIndividualFromClass(String clazz, String individualName) { 
    [...] // 参数校验
    Optional<OWLClassAssertionAxiom> individualAssertionOpt =
            ontology
                    .getClassAssertionAxioms(clazz)
                    .stream()
                    .filter(
                            i -> i.getIndividual().asOWLNamedIndividual().getIRI().getRemainder().orElse("").matches(individualName)
                    )
                    .findFirst();

    if (!individualAssertionOpt.isPresent())
        return false;
    else {
        ChangeApplied changed = ontology.remove(individualAssertionOpt.get());

        return changed.equals(ChangeApplied.SUCCESSFULLY) || changed.equals(ChangeApplied.NO_OPERATION);
    }
}

检测个体是否属于某类的方法 #

public boolean doesIndividualBelongToClass(String className, String name) {
    [...] // 参数校验及获取'clazz'
    Set<OWLNamedIndividual> inferredIndividuals =
            reasoner
                    .getInstances(clazz, false)
                    .getFlattened()
                    .stream()
                    .filter(i -> i.getIRI().getRemainder().orElse("").equals(name))
                    .collect(Collectors.toSet());

    Set<OWLNamedIndividual> assertedIndividuals = ontology
            .individualsInSignature()
            .filter(i -> i.getIRI().getRemainder().orElse("").equals(name))
            .filter(
                    i -> reasoner
                            .getTypes(i)
                            .entities()
                            .filter(t -> t.getIRI().getRemainder().orElse("").equals(className))
                            .findFirst()
                            .isPresent()
            ).collect(Collectors.toSet());

    inferredIndividuals.addAll(assertedIndividuals);

    return inferredIndividuals
            .stream()
            .findFirst()
            .isPresent();
}

检测个体是否存在的方法 #

public boolean doesIndividualExist(String login)  {
    return doesIndividualBelongToClass("owl:Thing", login);
}

问题细节 #

删除类断言后，doesIndividualBelongToClass("Person", login)返回false，但doesIndividualExist(login)返回true。调试发现该个体仍被推理器视为owl:Thing的实例；用reasoner.isSatisfiable()查询该个体的可满足性，结果为可满足，但保存本体后用Protege查看，该个体已不存在。

问题分析 #

1. OWL语义特性：owl:Thing是所有个体的默认父类，只要个体存在于本体签名中（即出现在任意公理里），推理器会默认其属于owl:Thing。当前删除方法仅移除了个体的Person类断言，若该个体还存在于其他公理（如属性断言）中，会留在本体签名里。
2. 推理器状态同步问题：即使移除了所有相关公理，HermiT的内部缓存可能未彻底清理，仅调用flush()（即封装的think()）无法完全重置推理状态。
3. 存在性检测逻辑缺陷：doesIndividualExist依赖owl:Thing实例检测，而推理器会将所有签名中的个体都推断为owl:Thing实例，哪怕没有显式断言。

解决方案 #

1. 彻底移除个体的所有相关公理 #

删除个体时，不能只移除类断言，要遍历删除所有包含该个体的公理：

public boolean removeIndividual(String individualName) {
    [...] // 参数校验，获取目标OWLNamedIndividual实例
    // 获取所有包含该个体的公理
    Set<OWLAxiom> axiomsToRemove = ontology.getReferencingAxioms(targetIndividual);
    boolean hasRemoved = false;
    for (OWLAxiom axiom : axiomsToRemove) {
        ChangeApplied result = ontology.remove(axiom);
        if (result.equals(ChangeApplied.SUCCESSFULLY)) {
            hasRemoved = true;
        }
    }
    return hasRemoved;
}

2. 重置推理器实例 #

删除个体并更新本体后，直接重新创建推理器，避免内部缓存残留：

// 替换原有的ontology.think()逻辑
reasoner.dispose();
reasoner = new ReasonerFactory().createReasoner(ontology);

3. 调整存在性检测逻辑 #

不依赖owl:Thing实例检测，直接检查本体签名+个体可满足性：

public boolean doesIndividualExist(String login) {
    OWLNamedIndividual target = dataFactory.getOWLNamedIndividual(individualName, prefixManager);
    // 先检查本体签名中是否存在该个体
    boolean inSignature = ontology.individualsInSignature().anyMatch(i -> i.equals(target));
    if (!inSignature) {
        return false;
    }
    // 再检查该个体是否可满足（避免隐式推断的个体）
    OWLClass oneOf = dataFactory.getOWLObjectOneOf(target);
    return reasoner.isSatisfiable(oneOf);
}

内容的提问来源于stack exchange，提问作者Chaos