OWL属性关联的通用类不相交公理是否依赖类本身不相交

核心判定规则 #

两个类的不相交公理生效的核心逻辑是：不存在任何个体可以同时被归为这两个类的实例，符合OWL DL规范的推理机（如HermiT）只要检测到同时属于两个不相交类的个体，就会抛出本体不一致错误。

测试场景复盘 #

场景1（正确配置版本） #

• 类定义：A、B
• 对象属性：hasValue
• 通用类公理：hasValue some A disjointWith hasValue some B
• 个体：user1
• 个体断言：user1 hasValue A、user1 hasValue B

该配置下推理机必然抛出不一致错误：个体:A是类A的实例，个体:B是类B的实例，user1同时关联两个个体，会被同时归为hasValue some A和hasValue some B两个类的实例，直接触发不相交公理的冲突判定。
最初测试未报错的原因是公理编写存在偏差，并非公理本身不生效。

场景2 #

• 类定义：A、B，额外声明类公理A disjointWith B
• 对象属性：hasValue
• 通用类公理：hasValue some A disjointWith hasValue some B
• 个体：user1
• 个体断言：user1 hasValue A、user1 hasValue B

该场景下存在两层冲突触发点：第一层是user1同时属于两个不相交的限制类；第二层是个体A、B本身属于两个互斥的类，user1同时关联二者也会触发类层面的不相交冲突，因此推理机必然报错。

公理不等价性验证 #

以下两条公理不存在等价关系，推理结果完全不同：

• hasValue some B DisjointWith hasValue some A
  该公理要求：不存在任何个体可以同时存在一个类型为B的hasValue取值、和一个类型为A的hasValue取值，只要个体同时关联A、B类的实例就会触发冲突。
• hasValue some B DisjointWith hasValue some (P and (not (B)))
  该公理要求：不存在任何个体可以同时存在一个类型为B的hasValue取值、和一个类型为P但不属于B的hasValue取值。受OWL开放世界假设影响，在未额外声明A与B不相交的前提下，推理机不会默认判定A类个体属于not B的范畴——即存在A的个体同时是B的个体的可能，因此user1同时关联A、B实例不会触发冲突，本体保持一致。

测试用完整本体代码 #

@prefix : <http://test.org/#> .
@prefix owl: <http://www.w3.org/2002/07/owl#> .
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix xml: <http://www.w3.org/XML/1998/namespace> .
@prefix xsd: <http://www.w3.org/2001/XMLSchema#> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
@base <http://test.org/> .

<http://test.org/> rdf:type owl:Ontology .

#################################################################
#    对象属性定义
#################################################################

###  http://test.org/#hasValue
:hasValue rdf:type owl:ObjectProperty .


#################################################################
#    类定义
#################################################################

###  http://test.org/#A
:A rdf:type owl:Class ;
   rdfs:subClassOf :P .


###  http://test.org/#B
:B rdf:type owl:Class ;
   rdfs:subClassOf :P .


###  http://test.org/#P
:P rdf:type owl:Class .


###  http://test.org/#USER
:USER rdf:type owl:Class .


#################################################################
#    个体定义
#################################################################

###  http://test.org/#A
:A rdf:type owl:NamedIndividual ,
            :A .


###  http://test.org/#B
:B rdf:type owl:NamedIndividual ,
            :B .


###  http://test.org/#user1
:user1 rdf:type owl:NamedIndividual ;
       :hasValue :A ,
                 :B .


#################################################################
#    通用类公理
#################################################################

[ rdf:type owl:Restriction ;
  owl:onProperty :hasValue ;
  owl:someValuesFrom :A ;
  owl:disjointWith [ rdf:type owl:Restriction ;
                     owl:onProperty :hasValue ;
                     owl:someValuesFrom [ owl:intersectionOf ( :P
                                                               [ rdf:type owl:Class ;
                                                                 owl:complementOf :A
                                                               ]
                                                             ) ;
                                          rdf:type owl:Class
                                        ]
                   ]
] .


[ rdf:type owl:Restriction ;
  owl:onProperty :hasValue ;
  owl:someValuesFrom :B ;
  owl:disjointWith [ rdf:type owl:Restriction ;
                     owl:onProperty :hasValue ;
                     owl:someValuesFrom [ owl:intersectionOf ( :P
                                                               [ rdf:type owl:Class ;
                                                                 owl:complementOf :B
                                                               ]
                                                             ) ;
                                          rdf:type owl:Class
                                        ]
                   ]
] .


###  Generated by the OWL API (version 4.5.9.2019-02-01T07:24:44Z)

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