Automated Reasoning with Legal Entities

A research project funded by the

Luxembourg National Research Fund

Grant: CORE C20/IS/14616644

AuReLeE conclusion workshop on July 15 - July 22, onlne and in presence at the DCS at Univ. of Luxembourg.

Featuring keynotes of Christoph Benzmüller (U Bamberg) and Geoff Sutcliffe (Univ. of Miami), Alexander Steen (U Greifswald) and many more.

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 (University of Greifswald, proposer of AuReLeE and PI)
David Fuenmayor (Research and development specialist)


Leon van der Torre (University of Luxembourg)


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. A. Steen, D. Fuenmayor, T. Gleißner, G. Sutcliffe, C. Benzmüller, Automated Reasoning in Non-classical Logics in the TPTP World. In Proceedings of the 8th Int. Workshop on Practical Aspects of Automated Reasoning (PAAR-2022),, 2022. Accepted for publication.
  2. A. Steen, An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning. In Proceedings of the 8th Int. Workshop on Practical Aspects of Automated Reasoning (PAAR-2022),, 2022. Accepted for publication.
  3. Alexander Steen, David Fuenmayor, A Formalisation of Abstract Argumentation in Higher-Order Logic. Journal of Logic and Computation, 2022. In print. Preprint available at arXiv:2110.09174 [cs.AI].
  4. A. Adrian, M. Rapp, A. Steen, Von Objekt- und Meta-Ebenen: Analyse der Softwareanforderungen computergestützter juristischer Entscheidung.. In In Recht DIGITAL – 25 Jahre IRIS, Proceedings of 25th Internationales Rechtsinformatik Symposion (IRIS 2022), Editions Weblaw, 2022.
  5. 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.
  6. 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), College Publications, 2021.

Further related publications

  1. W. Carnielli, M. Coniglio, D. Fuenmayor, Logics of formal inconsistency enriched with replacement: an algebraic and modal account. Review of Symbolic Logic, online first, 2021.
  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.
  4. < C. Nalon, A. Steen, Guest Column: It is dark before dawn. In Association for Automated Reasoning, Newsletter No. 136, November 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: June 2022