Every ODRL 2.2 constraint compares a single scalar value: (leftOperand, operator, rightOperand). Five of ODRL's approximately 34 left operands, however, denote multi-dimensional quantities--image dimensions, canvas positions, geographic coordinates--whose specification text explicitly references multiple axes. For these operands, a single scalar constraint admits one interpretation per axis, making policy evaluation non-deterministic. We classify ODRL's left operands by value-domain structure (scalar, dimensional, concept-valued), grounded in the ODRL 2.2 specification text, and show that dimensional ambiguity is intrinsic to the constraint syntax. We present an axis-decomposition framework that refines each dimensional operand into axis-specific scalar operands and prove four properties: deterministic interpretation, AABB completeness, sound over-approximation under projection, and conservative extension. Conflict detection operates in two layers: per-axis verdicts are always decidable; box-level verdicts compose through Strong Kleene conjunction into a three-valued logic (Conflict, Compatible, Unknown). For ODRL's disjunctive (odrl:or) and exclusive-or (odrl:xone) logical constraints, where per-axis decomposition does not apply, the framework encodes coupled multi-axis conjectures directly. We instantiate the framework as the ODRL Spatial Axis Profile--15 axis-specific left operands for the five affected base terms--and evaluate it on 117 benchmark problems spanning nine categories across both TPTP FOF (Vampire) and SMT-LIB (Z3) encodings, achieving full concordance between provers. Benchmark scenarios are inspired by constraints arising in cultural heritage dataspaces such as Datenraum Kultur. All meta-theorems are mechanically verified in Isabelle/HOL.


翻译:每个ODRL 2.2约束都涉及单个标量值的比较:(左操作数,运算符,右操作数)。然而,在ODRL约34个左操作数中,有5个表示多维量——图像尺寸、画布位置、地理坐标——其规范文本明确引用了多个坐标轴。对于这些操作数,单个标量约束在每个轴上允许一种解释,导致策略评估具有非确定性。我们基于ODRL 2.2规范文本,按值域结构(标量型、维度型、概念值型)对ODRL左操作数进行分类,并证明维度歧义是约束语法固有的特性。我们提出了一个轴分解框架,将每个维度型操作数细化为轴特定的标量操作数,并证明了四个性质:确定性解释、AABB完备性、投影下的可靠过近似,以及保守扩展。冲突检测在两层进行:单轴判定总是可判定的;箱型层级判定通过强克莱尼合取组合成三值逻辑(冲突、兼容、未知)。对于ODRL中不适用单轴分解的析取(odrl:or)与异或(odrl:xone)逻辑约束,该框架直接编码耦合的多轴猜想。我们将该框架实例化为ODRL空间轴配置文件——为五个受影响的基项定义了15个轴特定左操作数——并在117个基准问题上进行评估,这些问题涵盖TPTP FOF(Vampire)和SMT-LIB(Z3)两种编码方式的九类场景,实现了证明器间的完全一致性。基准场景的灵感来源于文化遗产数据空间(如Datenraum Kultur)中出现的约束。所有元定理均在Isabelle/HOL中进行了机械化验证。

0
下载
关闭预览

相关内容

专知会员服务
15+阅读 · 2021年9月29日
图节点嵌入(Node Embeddings)概述,9页pdf
专知
15+阅读 · 2020年8月22日
多因素问题分析时,如何确立各因素权重?
人人都是产品经理
75+阅读 · 2020年3月4日
标签间相关性在多标签分类问题中的应用
人工智能前沿讲习班
23+阅读 · 2019年6月5日
使用 Canal 实现数据异构
性能与架构
20+阅读 · 2019年3月4日
图分类:结合胶囊网络Capsule和图卷积GCN(附代码)
中国人工智能学会
36+阅读 · 2019年2月26日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
5+阅读 · 2014年12月31日
国家自然科学基金
6+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
VIP会员
最新内容
 军事通信系统与设备的技术演进综述
专知会员服务
0+阅读 · 16分钟前
《北约标准:医疗评估手册》174页
专知会员服务
0+阅读 · 24分钟前
《提升生成模型的安全性与保障》博士论文
专知会员服务
0+阅读 · 28分钟前
美国当前高超音速导弹发展概述
专知会员服务
4+阅读 · 4月19日
无人机蜂群建模与仿真方法
专知会员服务
8+阅读 · 4月19日
澳大利亚发布《国防战略(2026年)》
专知会员服务
2+阅读 · 4月19日
全球高超音速武器最新发展趋势
专知会员服务
3+阅读 · 4月19日
相关VIP内容
专知会员服务
15+阅读 · 2021年9月29日
相关基金
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
5+阅读 · 2014年12月31日
国家自然科学基金
6+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
Top
微信扫码咨询专知VIP会员