英文:
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
是的,本体是一致的。你对∃-规则的应用几乎是正确的,确实,你需要引入一个新的命名个体作为x
的s
-后继,比如说z
- 正如你所做的。而且你还需要引入一个新的命名个体作为y
的s
-后继,比如说w
。
因此,你需要引入2个新的命名个体。你不能重用一个已经引入的命名个体作为两个不同个体的后继。这是因为在一个更大的本体中,x
和y
可能有其他关于它们的断言或公理,这些可能对它们施加额外的约束,如果你假设它们有相同的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.
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库,让每个人都能够通过互相帮助和分享经验来进步。
评论