protege reasoner 不报告违反 GCI 的错误 [英] protege reasoner not report error for violation of GCI

问题描述

我目前使用 Protege 构建本体的主要目标是一致性检查.为此，我从小型测试开始.

My main goal with Protege an ontology building at present is consistency checking. To that end I'm starting with small tests.

在这种情况下，我想坚持认为具有特定属性的类的任何实例"都必然具有另一个属性.

In this case I want to insist that any "instance" of a class with a certain property necessarily has another property.

按照这个很久以前的帖子 我写了以下GCI:

Following this thread from a long time ago I wrote the following GCI:

expression and (structureType value structureItem) SubClassOf hasAuthor min 1 person

我的意思是说:任何具有属性 structureType 其值为 structureItem 的 expression 类必须具有或必须至少有一个属性 hasAuthor

By this I mean to state that: any class that is an expression that has the property structureType whose value is structureItem must have or necessarily has at least one property hasAuthor

但是当我在 Protege 中使用这样一个 expression 而没有 hasAuthor 属性运行推理器时，我没有收到任何错误.

But when I run the reasoner in Protege with such an expression WITHOUT a hasAuthor property I don't get any error.

我的规则是否有问题，或者我是否期望推理器提供它并非旨在做的事情.

Is there something wrong with my rule or am I expecting something from the reasoner that it is not designed to do.

推荐答案

发生的事情与开放世界假设无关.稍后会详细介绍.

What happens has nothing to do with Open World Assumption. More on that later.

为了显示推理器的行为是多么正常，让我稍微简化一下您的 GCI.让我们考虑类 Father 和属性 hasChild 以及以下 GCI:

In order to show how normal the reasoner is behaving, let me simplify a bit your GCI. Let's consider the class Father and the property hasChild and the following GCI:

Father  SubClassOf  hasChild min 1

这是说父亲至少有一个孩子.这是常识性知识.现在，如果我补充一个事实:

This is saying that fathers have at least one child. This is common sense knowledge. Now, if I add the fact that:

Antoine  Type  Father

您的问题表明应该将其检测为错误.如果您考虑一下我们在这里所代表的知识，应该很清楚将其解释为错误是违反正常推理的.如果我遇见你并告诉你:

your question suggests that it should be detected as an error. If you think about the knowledge we are representing here, it should be clear that interpreting this as an error is going against normal reasoning. If I meet you and tell you:

安托万是父亲！你知道，父亲至少有一个孩子.

Antoine is a father! You know, fathers have at least one child.

你可能不会吃惊地说:

你错了，安托万！

因为我所说的只是简单、一致、合理的知识.OWL 是一种知识表示语言.每个人都知道的合理和一致的东西在OWL中是合理和一致的.OWL 不会因未说明的义务而造成错误.subClassOf 关系不是为了能够在子类中而提供在超类中的证明的义务.GCI 只是提供了有关它所描述的世界的一些真相.所以如果我说安托万是父亲，那么我可以得出结论，安托万有一个孩子，就这么简单.

because what I say is just plain, consistent, reasonable knowledge. OWL is a knowledge representation language. What is reasonable and consistent in everyone's knowledge is reasonable and consistent in OWL. OWL does not create errors from unsaid obligations. A subClassOf relation is not an obligation to provide the proof of being in the superclass in order to be able to be in the subclass. A GCI just provides some truth about the world it describes. So if I state that Antoine is a father, then I can conclude that Antoine has a child, it's as simple as that.

您可能将概念包含与某种约束混淆了.但是将 GCI 解释为这样的约束或义务完全违背了本体论的目的.如果您有:

You are probably confusing concept inclusions with some sort of constraint. But interpreting GCIs as such constraints or obligation completely defies the purpose of ontologies. If you have:

StackOverflowUser  SubClassOf  Person
Jeff  Type  StackOverflowUser

你必须证明杰夫确实是一个人才能避免系统抛出错误?！所以你必须把应该是合乎逻辑的结论作为明确的事实.这与推理和推理的想法相反！

you would have to prove that Jeff is indeed a person to avoid the system throwing an error?! So you would have to put what ought to be logical conclusions as explicit facts. That's the opposite of the idea of reasoning and inferences!

现在，让我们回到 OWA.必须澄清 OWA 是什么，不是什么.

Now, let us go back to OWA. Some clarification about what OWA is, and is not, must be made.

首先，令人惊讶的是，开放世界假设并非假设.如此命名是为了满足封闭世界假设 (CWA) 和不存在封闭世界假设之间的相似之处的令人愉悦的美学.封闭"的互补是开放"，所以封闭世界假设的对立面一定是开放世界假设.

First, surprisingly, the Open World Assumption is not an assumption. It is named so in order to satisfy the pleasing esthetics of the parallel between Closed World Assumption (CWA) and the absence of Closed World Assumption. The complementary of "Closed" is "Open", so it must be the case that the opposite of Closed World Assumption is Open World Assumption.

但是将没有假设的情况称为假设"是错误的.所以这就引出了一个问题什么是封闭世界假设?"然后.

But it would be a mistake to qualify as an "assumption" the absence of an assumption. So this begs the question "what is the Closed World Assumption?" then.

CWA 是一阶逻辑 (FOL) 的概念，在数据库理论的背景下定义.数据库通常保存肯定语句"的记录——可以将其形式化为 FOL 原子，如 hasChild(Antoine, R.)——但不是否定语句"——形式化为诸如 ¬hasChild(Antoine, Jeff).在一个家谱记录数据库中，记录所有的事物对 x 和 y 使得 ¬hasChild(x, y).相反，可以合理地假设如果 hasChild(x, y) 不存在于数据库中，那么它遵循 ¬hasChild(x, y).这就是 CWA 的精髓.

CWA is a concept of first order logic (FOL), defined in the context of database theory. Databases usually keep records of "positive statements" -- which can be formalised as FOL atoms like hasChild(Antoine, R.) -- but not "negative statements" -- formalised as negative literals like ¬hasChild(Antoine, Jeff). In a database of genealogical records, it would be insane to keep a record of all the pairs of things x and y such that ¬hasChild(x, y). Instead, it is reasonable to assume that if hasChild(x, y) is not present in the database, then it follows that ¬hasChild(x, y). This is the essence of CWA.

然而，这需要进一步澄清，因为它经常被调用 OWA/CWA 的人误解.有些人将 CWA 定义为这样一种假设，即不能从知识库或本体推导出来的东西被认为是错误的.这不是 CWA.如果是这样，那么每当我们不能得出 φ 和 ¬φ 的结论时，我们就会假设 φ 和 ¬φ 都是假的，这是矛盾的.因此，CWA 的真正形式化(由 Raimond Reiter 在 1978 年定义，并由数十年来数据库科学家和逻辑学家形式化)如下:

However, this needs further clarification, as it is often misinterpreted by people invoking OWA/CWA. Some people define CWA as the assumption that what cannot be deduced from a knowledge base or ontology is assumed to be false. This is not CWA. If it were the case, then whenever we cannot conclude φ nor ¬φ, we would assume that both φ and ¬φ are false, which is a contradiction. So the true formalisation of CWA (as defined by Raimond Reiter in 1978, and as formalised by database scientists and logicians for many decades) is the following:

如果不存在正基础文字的证明，则假定该文字的否定为真"[R.Reiter, On Closed World Databases, 1978]

"if no proof of a positive ground literal exists, then the negation of that literal is assumed true" [R. Reiter, On Closed World Data Bases, 1978]

更完整地，给定一个 FOL 理论 T，T 的封闭世界理论 CW(T) 是理论 T ∪ {¬φ |φ 是基原子，T ⊬ φ}.在理论 T 上制作 CWA 意味着使用 CW(T) 而不是 T 进行推理，用于逻辑推论或查询回答.

More completely, given a FOL theory T, the closed world theory CW(T) of T is the theory T ∪ {¬φ | φ is a ground atom and T ⊬ φ}. Making the CWA on a theory T means reasoning with CW(T) instead of T for the purposes of logical deductions or query answering.

理论上 T = {∀x.Father(x) → ∃y.hasChild(x>,y), Father(Antoine)}，CWA 得出结论 ¬hasChild(Antoine, Antoine), ¬hasChild(Antoine, Jeff) 等，但不会导致 Error(T)，也不认为 CW(T) 不一致.

On the theory T = {∀x.Father(x) → ∃y.hasChild(x,y), Father(Antoine)}, the CWA leads to the conclusions ¬hasChild(Antoine, Antoine), ¬hasChild(Antoine, Jeff), etc. but not to Error(T), nor to that CW(T) is inconsistent.

总而言之，如果 CWA 与 T 是否有错误或不一致无关，那么 OWA 也是如此.我不知道 Ivo Velitchkov 和 Stanislav Kralin 在提到 OWA 时想到的是什么，但无论是什么，对于我所知道的关于该主题的科学文献来说都是陌生的.

In conclusion, if CWA is irrelevant to whether T has an error or is inconsistent, then so is OWA. I don't know what Ivo Velitchkov and Stanislav Kralin have in mind when they refer to OWA, but whatever it is, it is foreign to the scientific literature on the topic that I'm aware of.

这篇关于protege reasoner 不报告违反 GCI 的错误的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！