Automated Reasoning with Legal Entities

A research project funded by the

Luxembourg National Research Fund

Grant: CORE C20/IS/14616644

AuReLeE kick-off event on May 27, 9am (CEST), online via WebEx

Featuring talks of Prof. Adam Wyner (Swansea Univ.) and Prof. Leon van der Torre (Univ. of Luxembourg), and further contributed talks.

Learn more & join

About the project

Automated reasoning systems are symbolic AI systems for autonomously assessing the correctness of formally specified information. Such tools are provided by the user with the information to be assessed in some textual representation, and subsequently search for a formal justification of a given claim without additional guidance from the outside. Application areas include computer-assisted mathematics, knowledge discovery and processing, computer linguistics, semantic web, and software and hardware verification. As an example of such systems, so-called SAT and SMT solvers are highly successful in both research and industry, and became standard tools for various software and hardware production chains.

In legal informatics, computer systems are used for assisting professionals and public regulators for, e.g., structuring and assessing normative contents, and for improved search in large knowledge bases. In legal reasoning, a sub-field of legal informatics, a current challenge is to design and implement reasoning technology for assisting legal drafting, for conducting (semi-)automated compliance checks, and further practically relevant applications. Usually, a first step in this process is the formalization of normative structures in knowledge bases. However, the practical utilization of these valuable knowledge bases is then often quite limited. This is, to a large extent, due to the lack of suitable computational methods that would allow the assessment and mechanized utilization of the normative information compiled by these knowledge bases.

The goal of the project Automated Reasoning with Legal Entities (AuReLeE) is thus to provide effective and general means for the automation of normative reasoning processes based on legal knowledge bases. To this end, the project will design and implement a dedicated system that combines efficient decision procedures with a flexible approach to import and re-use existing knowledge bases for their employment as underlying contexts for the normative reasoning tasks. The results of AuReLeE hence allow to full utilization of the existing legal knowledge bases’ potential for compliance checking.

AuReLeE is conducted at the Faculty of Science, Technology and Medicine of the University of Luxembourg. It is hosted by the Individual and Collective Reasoning (ICR) research group at the Depart of Computer Science.

The team

Core team

Alexander Steen (Principal investigator)
David Fuenmayor (Research and development specialist)

Advisory board

Leon van der Torre (University of Luxembourg, local advisor)
Adam Wyner (Swansea University, mentor)


All the software and code produced within the AuReLeE project is open-source and freely available (usually under MIT or BSD-like license) at GitHub: . Highlighted artifacts (repositories) are listed in the following.

rio: A reasoner for I/O logics [ aureleeNet/rio]

rio is an automated reasoning system for unconstrained and constrained I/O logics based on propositional logic. It is implemented as a Scala application.

In short, the system allows you to specify a set of conditional norms and a number of inputs (each of which describing aspects of the current situational context), and provides automated means for inferring whether given obligations (also encoded as formulas) can be derived. rio can also be used to infer the set of detached obligations instead of checking detachment of given ones.

See the README for more details.

Isabelle/HOL Formalizations: Embeddings and experiments [ aureleeNet/formalizations]

This repository collects formalizations of different logical models in the context of normative reasoning and argumentation.


Core project publications

  1. Alexander Steen, Goal-Directed Decision Procedures for Input/Output Logics. In 15th International Conference on Deontic Logic and Normative Systems (DEON 2020/2021, Munich), Fenrong Liu, Alessandra Marra, Paul Portner, and Frederik Van De Putte (Eds.), College Publications, London, 2021. (to appear).

Further related publications

  1. D. Fuenmayor, A. Steen A Flexible Approach to Argumentation Framework Analysis using Theorem Proving. In First International Workshop on Logics for New-Generation Artificial Intelligence (LNGAI 2021), 2021. Accepted for publication
  2. A. Steen, C. Benzmüller, Extensional Higher-Order Paramodulation in Leo-III. Journal of Automated Reasoning, 2021.
  3. C. Benzmüller, D. Fuenmayor, Value-oriented Legal Argumentation in Isabelle/HOL. In International Conference on Interactive Theorem Proving (ITP), Proceedings, LIPIcs, Vol. 193(23), pp. 1-18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.


Please contact Alexander Steen for questions about the project.

AuReLeE acknowledges financial support from the Luxembourg National Research Fund (FNR) under grant CORE AuReLeE (C20/IS/14616644). Last updated: May 20, 2021