AuReLeE

Automated Reasoning with Legal Entities

A research project funded by the

Luxembourg National Research Fund

Grant: CORE C20/IS/14616644

AuReLeE Workshop

During the workshop Automated Reasoning with Legal Entities (AuReLeE) you will participate in a series of lectures by international researchers in the areas of computational logic, automated reasoning and legal informatics with the aim to investigate effective and general means for the automation of normative reasoning processes based on legal knowledge bases. (More information on: https://aurelee.net/)

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 workshop will take place on Friday 15 July to Friday 22 July - Campus Belval, MNO building, room 1.040.

Participation is open to anybody interested in the topics surrounding the project, i.e., including computational logic, normative reasoning, legal reasoning, automated theorem proving, software system standardization and development, AI & Law, KR, rule languages, and more. Feel free to forward this information to anybody that might be interested as well.

Confirmed speakers/key participants

  • Guillaume Aucher (Univ. Rennes)
  • Christoph Benzmüller (Univ. of Bamberg/FU Berlin)
  • David Fuenmayor (Univ. of Luxembourg)
  • Tobias Gleißner (Fraunhofer FOKUS)
  • Rajeev Goré (ANU)
  • Xavier Parent (TU Vienna)
  • Livio Robaldo (Swansea Univ.)
  • Alexander Steen (Univ. of Greifswald)
  • Geoff Sutcliffe (Univ. of Miami)
  • Adam Wyner (Swansea Univ.)

Schedule


Please note that the schedule may still change a bit.

Talks

Guillaume Aucher

Towards a generic theorem prover for non-classical logics

We introduce atomic and molecular logics. They are somehow 'universal'. Indeed, every logic such that its truth conditions are expressible in terms of first-order formulas is as expressive as an atomic or a molecular logic. We show how automatic display and Hilbert calculi can be defined for any atomic and molecular logics whose connectives are so-called 'universal'. We provide examples of such automatic proof calculi for already well-known logics such as modal logic and the Lambek calculus. We sketch a correspondence theory for atomic logics and molecular logics which allows us to extend the automatic generation of proof calculi to logics whose semantics are defined by specific conditions on the class of models. We apply these correspondence results to propositional logic and rediscover already well-known proof calculi for it.

Christoph Benzmüller

HOL, Universal Meta-Logical Reasoning in HOL and LogiKEy — A brief Introduction

In this talk, I will first explain some of the merits of classical higher-order logic (HOL) and give an overview of my own contributions to the field. Then, I will outline the universal meta-logical reasoning approach that I have been developing and promoting with colleagues for about 15 years to enable flexible automation of quantified non-classical logics within HOL reasoners. Finally, I will outline the multi-layered LogiKEy methodology and infrastructure that enables the exploration of knowledge representation and reasoning solutions in non-trivial application domains, where even the object logics of interest (and combinations thereof) become negotiable.

Tobias Gleißner

Machine-processable Norms for Autonomous Vehicles

We present our concept for formalizing norms and employing automated reasoning in autonomous driving applications. The quantity of norms in traffic is huge and to formalize norms at such scale, a domain expert will be able to use our computer-aided formalization tool that is currently under development.

Rajeev Goré (jww. Cormac Kikkert and Robert McArthur)

CEGAR-Tableaux: improved modal satisfiability via modal clause-learning and SAT

We present CEGAR-Tableaux, a tableaux-like method for propositional modal logics utilising SAT-solvers, modal clause-learning and multiple optimisations from modal and description logic tableaux calculi. We use the standard Counter-example Guided Abstract Refinement (CEGAR) strategy for SAT-solvers to mimic a tableau-like search strategy that explores a rooted tree-model with the classical propositional logic part of each Kripke world evaluated using a SAT-solver. Unlike modal encodings into SAT-solvers and modal resolution methods, we do not explicitly represent the accessibility relation but track it implicitly via recursion. By using ``satisfiability under unit assumptions'', we can iterate rather than ``backtrack'' over the satisfiable diamonds at the same modal level (context) of the tree model with one SAT-solver. By keeping modal contexts separate from one another, we add further refinements for reflexivity and transitivity which manipulate modal contexts once only. Our solver CEGARBox is, overall, the best for modal logics K, KT and S4 over the standard benchmarks, sometimes by orders of magnitude. It can now also handle all of the 15 logics in the modal cube as well as multimodal tense logic Kt(n) (AKA description logic ALCI). We believe that in the future, all tableaux calculi implementations will use CEGAR-Tableaux.

Xavier Parent

New developments in conditional deontic logic

Preference-based conditional deontic logic is a de facto standard for normative reasoning. It offers a simple solution to contrary-to-duty paradoxes and allows to represent norms with exceptions. In this talk, I bring together under one roof various weakenings of transitivity (of the betterness relation), and present axiomatisation results for them. Taking stock, I consider the general question of finding correspondences between modal axioms and properties (in the models). So far such correspondences have been established with pen and paper. I present joint work with C. Benzmueller regarding the automated verification of these correspondences in Isabelle/HOL.

Alexander Steen

Non-Classical Reasoning in the TPTP World

Non-classical logics are used in a wide spectrum of disciplines, including artificial intelligence, computer science, mathematics, and philosophy. The de-facto standard infrastructure for automated theorem proving, the TPTP World, currently supports only classical logics. This paper describes the latest extension of the TPTP World, providing languages and infrastructure for reasoning in non-classical logics. The extension integrates seamlessly with the existing TPTP World.

Geoff Sutcliffe

The TPTP World - Infrastructure for Automated Reasoning

The TPTP World is a well known and established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems for classical logics. The data, standards, and services provided by the TPTP World have made it increasingly easy to build, test, and apply ATP technology. This talk and tutorial reviews the core features of the TPTP World, describes key service components of the TPTP World and how to use them, and presents some successful applications.

Livio Robaldo

Taking stock of available technologies for compliance checking on first-order knowledge

This research analyses and compares some of the automated reasoners that have been used in recent research for compliance checking. The focus is on formalizations at the first-order level. Past literature on normative reasoning mostly focuses on the propositional level. However, the propositional level is of little usefulness for concrete LegalTech applications, in which compliance checking must be enforced on (large) sets of individuals. This paper formalizes a selected use case in the considered reasoners and compares the implementations. The comparison will highlight that lot of further research still need to be done to integrate the benefits featured by the different reasoners into a single standardized first-order framework. All source codes are available at https://github.com/liviorobaldo/compliancecheckers

Contact

If you want to participate please contact David Fuenmayor.

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