Table of Contents
Fetching ...

Axis Decomposition for ODRL: Resolving Dimensional Ambiguity in Policy Constraints through Interval Semantics

Daham Mustafa, Diego Collarana, Yixin Peng, Rafiqul Haque, Christoph Lange-Bever, Christoph Quix, Stephan Decker

TL;DR

An axis-decomposition framework is presented that refines each dimensional operand into axis-specific scalar operands and proves four properties: deterministic interpretation, AABB completeness, sound over-approximation under projection, and conservative extension.

Abstract

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.

Axis Decomposition for ODRL: Resolving Dimensional Ambiguity in Policy Constraints through Interval Semantics

TL;DR

An axis-decomposition framework is presented that refines each dimensional operand into axis-specific scalar operands and proves four properties: deterministic interpretation, AABB completeness, sound over-approximation under projection, and conservative extension.

Abstract

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.
Paper Structure (21 sections, 12 theorems, 13 equations, 5 tables)

This paper contains 21 sections, 12 theorems, 13 equations, 5 tables.

Key Result

Proposition 2.3

For a dimensional left operand $\ell$ with $\mathcal{V}_\ell = D_1 \times \cdots \times D_n$, the constraint $(\ell, \bowtie, v)$ with $v \in \mathbb{R}$ admits $n + 2$ distinct satisfaction conditions: $n$ axis-specific conditions $\pi_k(\ell(w)) \bowtie v$ for $1 \leq k \leq n$, plus two aggregate

Theorems & Definitions (42)

  • Definition 2.1: Constraint
  • Definition 2.2: Dimensional Left Operand
  • Proposition 2.3: Dimensional Insufficiency
  • proof
  • Proposition 2.4: KB Cannot Resolve Left-Operand Ambiguity
  • proof
  • Proposition 2.5: Vocabulary Alignment is Unsound
  • proof
  • Remark 2.6: Unit vs. Axis
  • Corollary 2.7: Necessity of Axis Decomposition
  • ...and 32 more