DBIS

Background

ODRL constraints specify the conditions under which policy rules apply. At an abstract level, an atomic constraint can be represented as a triple c = 〈l, op, r〉, where l denotes a left operand, op an operator, and r a right-operand value. Depending on the operand domain, constraints may express numerical comparisons, temporal restrictions, categorical relations, or membership and hierarchy relations. Atomic constraints can additionally be combined using logical operators such as and, andSequence, or, and xone [3,4].

Although ODRL provides standardized syntax and vocabulary, syntactic validity does not guarantee semantic consistency. Multiple constraints may be mutually incompatible, equivalent, redundant, partially overlapping, or related through entailment. Previous work has therefore investigated formal semantics and machine-interpretable reasoning for ODRL policies, including rule-based semantics and compliance checking [5,6]. These approaches demonstrate that policy interpretation can benefit from an explicit formal reasoning layer rather than relying exclusively on syntactic validation.

Formal verification has also been extensively investigated for access-control policy languages. SAT- and SMT-based approaches can translate policy relationships into logical decision problems and automatically determine properties such as consistency, equivalence, implication, and conflict [7,8]. These results provide a methodological foundation for representing selected ODRL constraint relations as satisfiability problems.

This becomes particularly relevant when ODRL policies are generated by LLMs. Tool-augmented language-model approaches such as ReAct and Toolformer demonstrate how language models can interact with external computational tools rather than performing every reasoning step internally [9,10]. More directly, SatLM shows that an LLM can translate natural-language problems into declarative logical specifications while delegating the actual constraint-solving process to an automated solver [11]. This separation between semantic interpretation by the LLM and deterministic reasoning by a formal backend motivates the architecture investigated in this thesis.

SMT solvers such as Z3 and cvc5 support satisfiability checking over theories including arithmetic, datatypes, arrays, and uninterpreted functions [12,13]. First-order theorem provers such as Vampire provide an alternative reasoning paradigm for first-order logical encodings [14]. The thesis will investigate how these solver technologies can be integrated into the ODRL Multi-Agent LLM framework to provide explicit and reproducible constraint reasoning.

Tasks

a) Classify ODRL constraints and define the supported reasoning scope

• Analyze the ODRL Information Model and Vocabulary to identify constraint structures, left operands, operators, datatypes, and logical constraint constructs relevant to policy generation [3,4].
• Classify ODRL constraints according to their reasoning domains, including numeric, temporal, spatial, language, purpose, and constraints requiring external ontology or knowledge-base semantics.
• Analyze which constraint pairs can be compared directly within a common domain and distinguish them from cross-domain, knowledge-dependent, or otherwise unsupported cases.
• Define the first-stage reasoning scope, focusing on self-contained numeric constraints and selected simple temporal constraints, together with explicit assumptions and boundaries.
• Define a common constraint-relation taxonomy for solver output, including conflict, entailment, equivalence, compatibility, partial overlap, and unknown.

b) Formalize constraint relations and encode them for automated reasoning

• Define formal interpretations of the selected ODRL constraint types as logical formulas over suitable value domains, including numeric comparisons, numeric intervals, equality relations, and selected temporal intervals.
• Formalize the relation categories introduced in Task (a) as satisfiability or entailment problems. For example, determine whether one constraint entails another by checking the unsatisfiability of the first constraint combined with the negation of the second.
• Implement solver-specific encodings using SMT-LIB for SMT backends such as Z3 and cvc5 [12,13].
• Investigate a corresponding first-order representation, for example using TPTP/TFF, for selected reasoning problems suitable for theorem provers such as Vampire [14].
• Normalize backend-specific results into a common solver result model that distinguishes logical outcomes such as sat, unsat, and unknown from operational outcomes such as timeout and backend error.
• Map normalized solver results back to the constraint-relation taxonomy defined in Task (a).

c) Integrate an external formal reasoner into the ODRL Multi-Agent LLM pipeline

• Analyze the existing ODRL Multi-Agent LLM architecture and identify suitable integration points where solver-backed reasoning can support policy validation, revision, and conflict explanation [1,2].
• Design a structured input interface for the reasoning component that captures information such as left operand, operator, right operand, datatype, unit, logical connector, and relevant rule context.
• Design a solver-independent output interface that returns the inferred constraint relation, solver status, involved constraints, and an explanation that can be consumed by downstream LLM agents.
• Implement a modular formal reasoning component capable of invoking one or more SMT backends and, where appropriate, theorem-proving backends.
• Investigate how backend agreement or disagreement can be represented explicitly rather than hidden from downstream agents.
• Ensure that unsupported constraints or constraints requiring external semantic knowledge are returned explicitly as unsupported or requires_external_semantics, instead of being assigned an unsupported relation through heuristic guessing.
• Integrate solver feedback into the policy-generation workflow so that the LLM agents can use deterministic reasoning results when validating or revising generated ODRL policies.

d) Evaluate reasoning correctness, coverage, robustness, and pipeline impact

• Construct a representative benchmark of ODRL constraint-reasoning cases based on the constraint classes and relation taxonomy defined in Task (a).
• Evaluate the formal reasoning component in terms of correctness, supported-case coverage, backend agreement, runtime behavior, and robustness against malformed or underspecified constraints.
• Compare solver-backed reasoning with the existing LLM-based reasoning behavior in the ODRL Multi-Agent LLM framework, particularly for cases involving conflict detection, entailment, overlapping restrictions, and unsupported semantic assumptions.
• Analyze whether external formal reasoning reduces false conflict detections, missed conflicts, or unjustified semantic conclusions produced by LLM-only reasoning.
• Perform systematic error and failure analysis for cases involving unsupported operators, solver-unknown results, parsing or translation errors, backend disagreement, and incomplete input specifications.
• Identify constraint categories that remain outside the supported scope, including more complex temporal combinations and constraints requiring external ontology or knowledge-base reasoning, and formulate directions for future extension.

References

[1] Peng, Y., Mustafa, D.M., Collarana, D., Lange, C., Decker, S.: AI Copilot for Semantic Conflict-Free Data Usage Policy Creation. Manuscript (2026).

[2] Mustafa, D.M., Nadgeri, A., Collarana, D., Arnold, B.T., Quix, C., Lange, C., Decker, S.: From Instructions to ODRL Usage Policies: An Ontology Guided Approach. In: Proceedings of the LLM+KG Workshop at VLDB 2024 (2024). https://www.vldb.org/workshops/2024/proceedings/LLM%2BKG/LLM%2BKG-15.pdf

[3] Iannella, R., Villata, S.: ODRL Information Model 2.2. W3C Recommendation, World Wide Web Consortium (2018). https://www.w3.org/TR/odrl-model/

[4] Iannella, R., Steidl, M., Myles, S., Rodríguez-Doncel, V.: ODRL Vocabulary & Expression 2.2. W3C Recommendation, World Wide Web Consortium (2018). https://www.w3.org/TR/odrl-vocab/

[5] Steyskal, S., Polleres, A.: Towards Formal Semantics for ODRL Policies. In: Bassiliades, N., Gottlob, G., Sadri, F., Paschke, A., Roman, D. (eds.) RuleML 2015. LNCS, vol. 9202, pp. 360–375. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21542-6_23

[6] De Vos, M., Kirrane, S., Padget, J., Satoh, K.: ODRL Policy Modelling and Compliance Checking. In: Fodor, P., Montali, M., Calimeri, F., Roman, D. (eds.) RuleML+RR 2019. LNCS, vol. 11784, pp. 36–51. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-31095-0_3

[7] Turkmen, F., den Hartog, J., Ranise, S., Zannone, N.: Analysis of XACML Policies with SMT. In: Focardi, R., Myers, A. (eds.) Principles of Security and Trust – POST 2015. LNCS, vol. 9036, pp. 115–134. Springer, Berlin, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46666-7_7

[8] Fisler, K., Krishnamurthi, S., Meyerovich, L.A., Tschantz, M.C.: Verification and Change-Impact Analysis of Access-Control Policies. In: Proceedings of the 27th International Conference on Software Engineering (ICSE 2005), pp. 196–205 (2005). https://doi.org/10.1109/ICSE.2005.1553562

[9] Yao, S., Zhao, J., Yu, D., Du, N., Shafran, I., Narasimhan, K., Cao, Y.: ReAct: Synergizing Reasoning and Acting in Language Models. In: 11th International Conference on Learning Representations (ICLR 2023) (2023). https://openreview.net/forum?id=WE_vluYUL-X

[10] Schick, T., Dwivedi-Yu, J., Dessì, R., Raileanu, R., Lomeli, M., Hambro, E., Zettlemoyer, L., Cancedda, N., Scialom, T.: Toolformer: Language Models Can Teach Themselves to Use Tools. In: Advances in Neural Information Processing Systems 36 (NeurIPS 2023) (2023). NeurIPS 2023 Proceedings

[11] Ye, X., Chen, Q., Dillig, I., Durrett, G.: SatLM: Satisfiability-Aided Language Models Using Declarative Prompting. In: Advances in Neural Information Processing Systems 36 (NeurIPS 2023) (2023). NeurIPS 2023 Proceedings

[12] de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Berlin, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

[13] Barbosa, H., Barrett, C., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., Nötzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A Versatile and Industrial-Strength SMT Solver. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13243, pp. 415–442. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-99524-9_24

[14] Kovács, L., Voronkov, A.: First-Order Theorem Proving and Vampire. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification – CAV 2013. LNCS, vol. 8044, pp. 1–35. Springer, Berlin, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_1