基于ALC Tableaux算法的本体一致性校验操作正确性问询

待检查本体 #

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

用户操作步骤 #

1. 利用C ⊑ A ⊓ B为节点x和y添加标签A、B，此时x和y的标签为{A, B, C}；
2. 对A ⊑ ∃s.¬B应用⊑规则，得到¬A ⊔ ∃s.¬B；
3. 由于x和y不能满足¬A，因此必须满足∃s.¬B；应用∃规则时，新增节点z作为x和y的s后继节点，标签为¬B。

问题解答 #

1. ∃规则应用是否正确？ #

不正确。核心问题在于对∃规则的误用：

• ALC Tableaux的∃规则要求：当节点u的标签包含∃s.C时，需先检查u已有的s后继节点是否满足C。如果已有后继节点的标签与C矛盾，直接触发冲突，不能随意新增节点。
• 针对节点x，已知s(x,y)，y是x的s后继，但y的标签包含B，与∃s.¬B要求的¬B矛盾，此时应直接判定冲突，而非新增节点z。
• 节点y的情况：y的标签包含A，因此需满足∃s.¬B，但题目中未给出y的s后继节点，这一步可以新增后继节点，但x的情况已经触发了不可调和的冲突，无需进行这一步。

2. 本体一致性结论是否正确？ #

不正确，该本体不一致。推导逻辑：

1. 由C(x)、C(y)结合C ⊑ A ⊓ B，可推导出x、y的标签均包含A和B；
2. 对x而言，A ⊑ ∃s.¬B要求x满足¬A ⊔ ∃s.¬B，但x已有A标签，因此必须满足∃s.¬B；
3. 已知s(x,y)，即y是x的s后继，那么y的标签必须包含¬B，但y的标签已经有B，B与¬B同时存在，产生矛盾冲突，说明该本体无法构建出无冲突的Tableaux，因此本体不一致。

内容的提问来源于stack exchange，提问作者Alex