OWL如何编写单条通用类公理实现hasValue取值类互斥约束

需求背景 #

需要编写单条OWL通用类公理（GCI）实现如下约束规则：

• 若某个体的hasValue属性取值属于类集合{A,B,C,D}中的任意类X，则该个体不能同时拥有属于{A,B,C,D}中除X外其余类的hasValue取值。

该规则原本可以通过4条独立的互斥公理实现，具体为：

1. hasValue some A DisjointWith hasValue some (B or C or D)
2. hasValue some B DisjointWith hasValue some (A or C or D)
3. hasValue some C DisjointWith hasValue some (A or B or D)
4. hasValue some D DisjointWith hasValue some (A or B or C)

要求将上述4条公理合并为单条公理，实现完全等价的约束效果。

单条公理实现（曼彻斯特语法） #

直接使用如下通用类公理即可，不需要额外定义辅助类：

Class: hasValue some (A or B or C or D)
  SubClassOf: (hasValue only A) or (hasValue only B) or (hasValue only C) or (hasValue only D)

逻辑说明 #

• 公理左侧hasValue some (A or B or C or D)会匹配所有至少存在一个hasValue取值落在{A,B,C,D}集合内的个体
• 公理右侧要求被匹配的个体，其所有hasValue取值必须完全属于A、B、C、D四个类中的某一个，不允许出现跨类的取值
• 约束效果和原4条互斥公理完全等价：如果某个体同时持有{A,B,C,D}中两个不同类的hasValue取值，会同时违反右侧所有only约束，直接被推理机判定为不一致。

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