为数字权利语言ODRL建立跨层级规范语义，明确权限与禁止的深层逻辑。
What Does ODRL Mean? A Cross-Level Ontological Grounding of Permissions, Prohibitions, and Duties in UFO-L
- 提出跨层级设计原则，区分行为层与能力层的法律地位
- 揭示权限在开放/封闭世界下定义不完整，仅覆盖实现义务
- 用形式化验证确保39个问题中逻辑一致性，适合法律与安全研究者
ODRL策略评估器虽能生成裁决结果，却未阐明策略所确立的规范立场、其背后隐含的权力结构，以及谁有权宣布规范被违反。本文提出跨层级设计原则：任何可被违反且有后果的规范语言，必须同时包含行为级地位（许可、义务、权利、无权利）和能力级地位（权力、从属、豁免、无能）。将该原则应用于ODRL，发现禁止具有可违犯性（即存在违反可能且有后果），而许可在行为参数上定义不完整（开放世界与封闭世界差异），且正式语义仅涵盖实现义务。通过将ODRL在UFO-L中进行本体论奠基，每个激活规则映射为一个简单法律关系，使法律地位覆盖范围从2个扩展至8个；原有评估器中隐含的违规宣告权被显式表示为“权力-从属”对。所有公理均在Isabelle/HOL中机械验证，并在Vampire、E和Z3下通过39个问题基准测试。
原文摘要 · Abstract (English)
ODRL policy evaluators produce verdicts, but say nothing about the normative positions a policy brings into existence, the authority structures those positions presuppose, or who holds the power to declare a norm violated. We formulate the Cross-Level Design Principle: any normative language with violable, consequential norms requires both conduct-level positions (Permission, Duty, Right, No right) and competence-level positions (Power, Subjection, Immunity, Disability). Applying this to ODRL, we establish that prohibition is sanctioned (violation possible and consequential), that permission is underspecified across its behaviour parameter (open vs. closed world), and that the formal semantics covers achievement obligations only. We ground ODRL in UFO-L, mapping each activated rule to a simple legal relator and extending coverage from two to eight legal positions; violation-declaration authority, implicit in every existing evaluator, becomes an explicit Power-Subjection pair. All axioms are mechanically verified in Isabelle/HOL and across a 39-problem benchmark under Vampire, E, and Z3.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。