Policies and legal texts encode the rules by which organizations operate: who may access what, what obligations arise from a contract, what penalties apply when commitments are not met. Their correct interpretation has significant legal, financial, and operational consequences.

For decades, the automated reasoning community has built powerful tools for analyzing such rules once expressed in formal language — solvers, model checkers, theorem provers, and policy analysis frameworks that provide deterministic, provable verdicts. In parallel, the legal informatics community has studied formalization from the opposite direction, establishing that legal texts carry layers of meaning — intent, context, precedent, deliberate vagueness — that resist naive translation into classical logic.

The persistent challenge has been the gap between these communities. Bridging natural language and formal language has required manual formalization by domain experts — slow, expensive, and unscalable. Controlled natural languages and domain-specific languages have narrowed the gap, but adoption remains limited because the effort still falls on human authors.

Large language models are now changing this equation. Recent results in AI-assisted mathematics show that language models can translate natural-language problems into formal representations, submit them to theorem provers, interpret the feedback, and iterate — achieving results that neither component could reach alone. This same pattern is emerging in policy analysis, contract interpretation, and regulatory compliance, creating a largely unexplored research frontier. This Dagtuhl Seminar brings together researchers from automated reasoning, legal informatics, NLP, and policy analysis to address the fundamental questions at this new intersection:

Faithful encoding of intent: How do we verify that a machine-generated formalization preserves the intended meaning of a legal or policy text — given that "intended meaning" is itself contested in law? What notions of refinement or equivalence apply to this translation?

Ambiguity as a first-class concern: Legal ambiguity is often deliberate — a negotiation tool that defers resolution of contested points. How should neurosymbolic systems detect and surface ambiguities rather than silently resolving them? When must ambiguity be preserved in the formal model?

Compositional reasoning: Amendments stack on contracts, policies inherit and override, multiple instruments apply simultaneously. What fragments of logic suffice for real-world policy and contract languages, and what is the complexity of reasoning over compositions of independently authored documents?

The explanation problem: Formal verdicts must be communicated in terms a lawyer or auditor can inspect and challenge, with full provenance from source text through formal model to conclusion.

Iterative neural-symbolic refinement: ´ The most promising architectures involve repeated interaction between language models and reasoning engines. What are the formal foundations — convergence, soundness, trust — for systems where neither component is individually sufficient?

Our goal is not to declare that legal reasoning can or should be automated, but to rigorously map where neurosymbolic methods help, where they fall short, and what new science is needed at the interface. The Dagstuhl format is uniquely suited to this kind of cross-disciplinary synthesis.

Creative Commons BY 4.0

Claudia Cauli, Ruzica Piskac, and Martin Schäf

This seminar qualifies for Dagstuhl's a LZI Junior Researchers program. Schloss Dagstuhl wishes to enable the participation of junior scientists with a specialization fitting for this Dagstuhl Seminar, even if they are not on the radar of the organizers. Applications by outstanding junior scientists are possible until June 26, 2026.