如何在本体中进行存在量化推理？

Question

我正在尝试计算本体中的存在量化推论，如下所示。给定本体：

Politician(Albert)
Politician(Bob)
related(Albert, Bob)

我想得到以下推论：

∃ related.Politician

我尝试通过在 OWLAPI 应用程序中使用 ELK 和 HermiT 推理器以及通过 Protégé 来做到这一点。然而，这些推理机似乎并没有计算这种特定类型的推论。

这是我的代码片段：

    /**
     * Compute the ontology along with the inferred consequences
     * @throws OWLOntologyCreationException
     */
    public void computeInferredOntology() throws OWLOntologyCreationException {
        logger.info("Computing inferences...");

        reasoner.precomputeInferences();

        logger.info("Creating axiom generators list...");

        // To generate an inferred ontology we use implementations of inferred axiom generators
        List<InferredAxiomGenerator<? extends OWLAxiom>> generators = new ArrayList<InferredAxiomGenerator<? extends OWLAxiom>>();
        generators.add(new InferredClassAssertionAxiomGenerator());
        generators.add(new InferredSubClassAxiomGenerator());
        generators.add(new InferredEquivalentClassAxiomGenerator());
        generators.add(new InferredEquivalentDataPropertiesAxiomGenerator());
        generators.add(new InferredEquivalentObjectPropertyAxiomGenerator());
        generators.add(new InferredDataPropertyCharacteristicAxiomGenerator());
        generators.add(new InferredSubDataPropertyAxiomGenerator());
        generators.add(new InferredSubObjectPropertyAxiomGenerator());
        // generators.add(new InferredDisjointClassesAxiomGenerator());
        // generators.add(new InferredPropertyAssertionGenerator());

        logger.info("Generating inferred ontology...");

        // Put the inferred axioms into a fresh empty ontology.
        inferredOntology = ontologyManager.createOntology();
        ontologyManager.addAxioms(inferredOntology, ontology.getAxioms());
        InferredOntologyGenerator inferredOntologyGenerator = new InferredOntologyGenerator(reasoner, generators);
        inferredOntologyGenerator.fillOntology(ontologyManager.getOWLDataFactory(), inferredOntology);
    }

我想知道是否有任何推理机可以处理这种推理。另外，这是某些特定算法的已知问题吗？

谢谢大家。

Answer 1

Hermit 和 Elk 都支持存在量词。问题是你认为它的工作方式与实际工作方式不同，无论是从 OWL 还是描述逻辑的角度来看。

推理者不会做出你期望的推论，至少有两个原因：

1. 推理者仅根据已知类别进行推理。

   ∃related.Politician

   是一个类表达式或匿名类 - 也就是说，它描述了一个类，但没有给出名称。在您的示例中

   Politician

   是一个类。推理机将推理限制为已知类，否则推理的数量是无限的。

2. 描述逻辑/OWL 推理器做出 3 种特定类型的推理，它们是：

(a) 分类，即

Politician SubClassOf Person

(b) 实例检查，即个体

bob

是

Politician

的实例。

(c) 可满足性检查，即检查类

Politician

是否被迫为空。如果本体中存在逻辑不一致，则类将被强制为空。举个例子，如果我们定义

Politician EquivalentTo Person and not Person

，那么政客是不可满足的。

请注意，您的推论不在此列表中，因此推理器无法推导出它。

我在我的博客上写了本体论和推理，特别是存在性限制这里。我还解释了描述逻辑的语义，这有助于人们理解推理机here所得出的推论。我假设观众没有逻辑知识。