英文:
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.
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论