cs.CLFeb 23, 2026

Denotational Semantics for ODRL: Knowledge-Based Constraint Conflict Detection

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

Organizations: RWTH Aachen University, Germany · Fraunhofer FIT, Sankt Augustin, Germany · University of Galway, Ireland

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

Abstract

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.

Figures & tables

ChallengeScenarioWithout frameworkWith framework
Single-KB grounding Can we compute ODRL’s set operators?Policy uses isPartOf , isA ; request uses eq . Three dimensions: spatial : France vs. Europe purpose : ScientificRes. vs. NonCommercial language : fr vs. deAll three return Unknown —engine sees incomparable stringsPer-dimension verdicts: Compatible (France ⪯\preceq Europe) Unknown (R&D ⊑\sqsubseteq ? NonComm.) Conflict (fr ⋢\not\sqsubseteq de)
Cross-dataspace composition Do multi-dimensional policies compose?BSB policy: 3 constraints. French request: 3 constraints. Compatibility requires all pairs to overlap.No mechanism to conjoin verdicts across operandsLanguage Conflict blocks entire request. Diagnostic isolates blocking dimension.
Cross-standard alignment What if each side uses a different KB?BSB uses GeoNames, DPV, BCP 47. French archive uses ISO 3166, GDPR taxonomy, ISO 639-3. Same scenario, different standards.Policies from different standards are mutually opaque—no interoperabilityConflicts preserved across KB pairs. Unmapped concepts degrade to Unknown , never to false Conflict .
Table 1: Four interoperability challenges illustrated through a single scenario: BSB permits European access to German-language manuscripts for non-commercial use; a French archive requests access from France, in French, for scientific research.
Left OperandODRL SpecificationDomainRelation⊥ ⁣ ⁣ ⁣⊥\perp\!\!\!\perp Source
language“A natural language”Taxonomic⊑\sqsubseteqOntology
purpose“A defined purpose”Taxonomic⊑\sqsubseteqOntology
industry“A defined industry sector”Taxonomic⊑\sqsubseteqOntology
fileFormat“A transformed file format”Taxonomic⊑\sqsubseteqOntology
media“Category of a media asset”Taxonomic⊑\sqsubseteqOntology
recipient“The party receiving the result”Taxonomic⊑\sqsubseteqOntology
Table 2: KB-dependent ODRL operands with semantic domain classification
[ ⁣[c1] ⁣]⊓[ ⁣[c2] ⁣][\![c_{1}]\!]\sqcap[\![c_{2}]\!]VerdictConjectureSZS [ 16 ]SMT
∅\emptysetConflict¬∃x(…)\neg\exists x(\ldots)Theoremunsat
S≠∅S\neq\emptysetCompatible∃x(…)\exists x(\ldots)Theoremunsat
⊤\topUnknowneitherCounterSatsat
Table 3: Conflict detection verdicts and their prover encodings. The negated-conjecture pattern maps each verdict to a unique SZS/SMT-LIB result pair.
Paper ResultIsabelle NameLocale
Lemma 1disj_order_consistencyknowledge_base
Theorem 2.1soundnessknowledge_base
Theorem 2.3runtime_soundnessknowledge_base
Theorem 2.2composition_soundness_*knowledge_base
Lemma 2conflict_propagationknowledge_base
Proposition 3kb_monotonicity_verdictkb_extension
Table 4: Paper results and Isabelle/HOL mechanization. 44 results , 0 sorry .
OperandKB∣C∣|C|Role
spatialGEO0004GeoNames (primary)
 GEO0013ISO 3166 (alignment)
 GEO002—UNA + negative partOf
purposeDPV00010W3C DPV (primary)
 DPV0016GDPR-derived (alignment)
 DPV002—Same-level UNA
Table 5: Knowledge bases and axiom files used in the benchmark suite. Original KBs provide primary domain knowledge; alternative KBs test cross-standard alignment; auxiliary files supply UNA axioms and structural edge cases.
ProblemRequest⊑\sqsubseteq branch?¬⊑\lnot\sqsubseteq other?Verdict
ODRL085nonCommRes✓explicitCompatible
ODRL086commRes✓absentUnknown
Table 6: XONE requires explicit negative axioms. Both problems test xone(commercial, nonCommercial) but with different request values. The asymmetric KB coverage produces different verdicts.
More in this topic

Policy Evaluation

Policy evaluation estimates the outcomes, value, risks, and fairness of decision rules before or after deployment.

See all 55 papers

Explore similar work

CardsList
Feb 23, 2026

Axis-Aligned Semantics for ODRL: Resolving Dimensional Ambiguity in Policy Constraints

The Open Digital Rights Language (ODRL) represents policy constraints as triples of a left operand, an operator, and a value. Several spatial operands, however, range over multi-axis domains such as width, height, and depth, while the constraint syntax provides no explicit axis identity. As a result, policy engines cannot determine whether multiple constraints apply to the same axis or different ones, making conflict detection unsound or incomplete. We resolve this ambiguity by axis decomposition, replacing multi-axis operands with axis-specific scalar operands over totally ordered domains. Each constraint then denotes an interval per axis and each policy an axis-aligned box, reducing conflict detection to box comparison. We define a three-valued semantics (Conflict, Compatible, Unknown), prove the decomposition sound and backward compatible with ODRL, instantiate it as ODRL Axis-Aligned Profile (OAAP), and validate it on a benchmark of 256 ODRL policy problems, each expressed in Turtle and compiled to first-order (TPTP) and SMT-LIB form, using Vampire, E, Z3, and cvc5.

Daham Mustafa, Diego Collarana, Sabrina Kirrane +5

RWTH Aachen University, Aachen, Germany · Fraunhofer FIT, Sankt Augustin, Germany · Vienna University of Economics and Business (WU), Vienna, Austria +1

Policy EvaluationAccess Control
AskPDF
Jun 23, 2026

What Does ODRL Mean? A Cross-Level Ontological Grounding of Permissions, Prohibitions, and Duties in UFO-L

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.

Daham M. Mustafa, Christoph Lange, Giancarlo Guizzardi +3

Fraunhofer FIT, Sankt Augustin, Germany · RWTH Aachen University, Aachen, Germany · University of Twente, The Netherlands +1

Deontic LogicLegal Reasoning
AskPDF
Mar 13, 2026

ODRL Policy Comparison Through Normalisation

The ODRL language has become the standard for representing policies and regulations for digital rights. However its complexity is a barrier to its usage, which has caused many related theoretical and practical works to focus on different, and not interoperable, fragments of ODRL. Moreover, semantically equivalent policies can be expressed in numerous different ways, which makes comparing them and processing them harder. Building on top of a recently defined semantics, we tackle these problems by proposing an approach that involves a parametrised normalisation of ODRL policies into its minimal components which reformulates policies with permissions and prohibitions into policies with permissions exclusively, and simplifies complex logic constraints into simple ones. We provide algorithms to compute a normal form for ODRL policies and simplifying numerical and symbolic constraints. We prove that these algorithms preserve the semantics of policies, and analyse the size complexity of the result, which is exponential on the number of attributes and linear on the number of unique values for these attributes. We show how this makes complex policies representable in more basic fragments of ODRL, and how it reduces the problem of policy comparison to the simpler problem of checking if two rules are identical.

Jaime Osvaldo Salas, Paolo Pareti, George Konstantinidis

University of Southampton, University Road, Southampton, SO17 1BJ, UK

Topic pending
AskPDF