LLM Reasoning 相关度: 7/10

Denotational Semantics for ODRL: Knowledge-Based Constraint Conflict Detection

Daham Mustafa, Diego Collarana, Yixin Peng, Rafiqul Haque, Christoph Lange-Bever, Christoph Quix, Stephan Decker
arXiv: 2602.19883v1 发布: 2026-02-23 更新: 2026-02-23

AI 摘要

提出ODRL约束的指称语义,用于知识库驱动的策略冲突检测,提升跨数据空间互操作性。

主要贡献

  • 提出了ODRL约束的指称语义
  • 实现了基于知识库的冲突检测框架
  • 验证了框架在多个知识库上的有效性

方法论

定义了ODRL约束到知识库概念集的映射,冲突检测简化为集合交集运算,并使用定理证明器和SMT求解器验证。

原文摘要

ODRL's six set-based operators -- isA, isPartOf, hasPart, isAnyOf, isAllOf, isNoneOf -- depend on external domain knowledge that the W3C specification leaves unspecified. Without it, every cross-dataspace policy comparison defaults to Unknown. We present a denotational semantics that maps each ODRL constraint to the set of knowledge-base concepts satisfying it. Conflict detection reduces to denotation intersection under a three-valued verdict -- Conflict, Compatible, or Unknown -- that is sound under incomplete knowledge. The framework covers all three ODRL composition modes (and, or, xone) and all three semantic domains arising in practice: taxonomic (class subsumption), mereological (part-whole containment), and nominal (identity). For cross-dataspace interoperability, we define order-preserving alignments between knowledge bases and prove two guarantees: conflicts are preserved across different KB standards, and unmapped concepts degrade gracefully to Unknown -- never to false conflicts. A runtime soundness theorem ensures that design-time verdicts hold for all execution contexts. The encoding stays within the decidable EPR fragment of first-order logic. We validate it with 154 benchmarks across six knowledge base families (GeoNames, ISO 3166, W3C DPV, a GDPR-derived taxonomy, BCP 47, and ISO 639-3) and four structural KBs targeting adversarial edge cases. Both the Vampire theorem prover and the Z3 SMT solver agree on all 154 verdicts. A key finding is that exclusive composition (xone) requires strictly stronger KB axioms than conjunction or disjunction: open-world semantics blocks exclusivity even when positive evidence appears to satisfy exactly one branch.

标签

ODRL 指称语义 知识库 冲突检测 策略

arXiv 分类

cs.CL cs.LO