Skip to content

Reasoning with laws

Jump to bottom Edit New page
Alicia Villanueva edited this page Nov 5, 2025 · 1 revision

Short description of the challenge

We speak of a computational law when that law is intended to be enforced by software through an automated decision-making process. As digital technologies evolve to offer more solutions for public administrations, we see an ever-increasing number of computational laws. Traditionally, law is written in natural language. Computational laws, however, suffer various complications when written in natural language, such as underspecification and ambiguity which lead to a diversity of possible interpretations to be made by the coder. These could potentially resultinto an uneven application of the law.

Resorting to formal languages to write computational laws is tempting. However, writing laws in a formal language leads to further complications, for example, incomprehensibility for non-experts, lack of explicit motivation of the decisions made, or difficulties in retrieving the data leading to the outcome.

Research team/s involved (or communities)

Barcelona Group on Pure and Applied Proof Theory

Main issues / open problems related to the challenge

  • Society must democratically determine the appropriate balance between natural and formal language in drafting of computational laws, taking into account the trade-offs between the enhancement of certain legal principles over others. (See poster)
  • Employing proof assistants to prove program correctness yields (as good as) zero-error software. It is important to note that the resulting software will be as good as the corresponding formal specification. The problem of whether the formal specification fully aligns with our intention cannot be solved by mathematical means. Between intention and a linguistic materialization of this intention, there is always a translation at work that will introduce uncertainty. (See poster)
  • Explainability is fundamentally descriptive focusing on the software’s functioning, but it does not provide insight into why a particular decision was reached in a specific context. Motivation, by contrast, seems to be inherently constructive. Motivation involves justifying the decision-making process by articulating the reasoning based on the relevant facts and the legal grounds of the specific decision made.

Techniques and technologies related to the challenge

  • Logic specifications and reasoning
  • Rule-based Artificial Intelligence
  • Proof-checkers
  • Verification tools

Example(s)

Other relevant information (external links, references, etc.)

Add a custom footer

list of tools

list of challenges

Clone this wiki locally