AuReLeE

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.

Core team

Alexander Steen (University of Greifswald, proposer of AuReLeE and PI)
David Fuenmayor (Research and development specialist)

Further

Leon van der Torre (University of Luxembourg)

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: github.com/aureleeNet . Highlighted artifacts (repositories) are listed in the following.

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

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

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), CEUR-WS.org, 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), CEUR-WS.org, 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.