ALC – 本体一致性检查

huangapple go评论58阅读模式
英文:

ALC - Ontology consistency checking

问题

I have to check whether the following ontology is correct using the ALC tableux algorithm.

A ⊑ ∃s.¬B
C ⊑ A ⊓ B
C(x)
C(y)
s(x,y)

So first i use 'C ⊑ A ⊓ B' to label x and y with A and B. So x and y now have the labels A, B, and C. Then i use the ⊑-rule for 'A ⊑ ∃s.¬B':

¬A ⊔ ∃s.¬B

Since ¬A can't be true for x and y, ∃s.¬B must be true. So i use ∃-rule that says that if there is no successor of s with label ¬B, you add this node. So there is now a node, e.g., z, that is a successor of x and y and has the label ¬B.

Am i right with applying the ∃-rule here? So in my considerations, the ontology is consistent.

英文:

I have to check whether the following ontology is correct using the ALC tableux algorithm.

A ⊑ ∃s.¬B
C ⊑ A ⊓ B
C(x)
C(y)
s(x,y)

So first i use C ⊑ A ⊓ B to label x and y with A and B. So x and y now have the lables A,B and C. Then i use the ⊑-rule for A ⊑ ∃s.¬B:

¬A ⊔ ∃s.¬B

Since ¬A cant be true for x and y, ∃s.¬B musst be true. So i use ∃-rule that says that if there is no successor of s with label ¬B you add this node. So there is now a node e.g. z that is a sucessor of x and y and has the label ¬B.

Am i right with appyling the ∃-rule here? So in my conisderations the ontology is consistent.

答案1

得分: 1

是的,本体是一致的。你对∃-规则的应用几乎是正确的,确实,你需要引入一个新的命名个体作为xs-后继,比如说z - 正如你所做的。而且你还需要引入一个新的命名个体作为ys-后继,比如说w

因此,你需要引入2个新的命名个体。你不能重用一个已经引入的命名个体作为两个不同个体的后继。这是因为在一个更大的本体中,xy可能有其他关于它们的断言或公理,这些可能对它们施加额外的约束,如果你假设它们有相同的s-后继,可能会导致不一致性。

英文:

Yes, the ontology is consistent. Your application of ∃-rule is almost correct in that yes, you need to introduce a new named individual as s-successor of x, say z - as you have done. And you have to also introduce a new named individual as s-successor of y, say w.

Thus, you have to introduce 2 new named individuals. You cannot reuse an introduced named individual as successor for 2 different individuals. The reason for this is that in a larger ontology, x and y may have other assertions or axioms that place additional constraints on them which may cause an inconsistency if you assume they have the same s-successor.

huangapple
  • 本文由 发表于 2023年6月15日 14:21:37
  • 转载请务必保留本文链接:https://go.coder-hub.com/76479645.html
匿名

发表评论

匿名网友

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen:

确定