Logical Modalities within the European AI Act: An Analysis
Lara Lawniczak, Christoph Benzmüller
TL;DR
The study addresses the challenge of formally representing the European AI Act's diverse modalities for normative reasoning. It adopts the LogiKEy framework, using Higher-Order Logic (HOL) as a unifying meta-logic to embed a range of logics (e.g., SDL, DDL, STIT) within Isabelle/HOL and leverage automated proof tools for reasoning. Key contributions include a modality catalog for the AI Act, mapping these modalities to candidate logics, and presenting initial HOL embeddings with proof and model-finding results, including successful encodings of Article 5 and CTDs and exploring agency representations with extended DDL variants. The work advances automated compliance reasoning by establishing a concrete formalisation path and highlighting current limitations (notably with agency constructs and infinite-model concerns in certain logics) and outlining future directions for broader, more robust formalisation.
Abstract
The paper presents a comprehensive analysis of the European AI Act in terms of its logical modalities, with the aim of preparing its formal representation, for example, within the logic-pluralistic Knowledge Engineering Framework and Methodology (LogiKEy). LogiKEy develops computational tools for normative reasoning based on formal methods, employing Higher-Order Logic (HOL) as a unifying meta-logic to integrate diverse logics through shallow semantic embeddings. This integration is facilitated by Isabelle/HOL, a proof assistant tool equipped with several automated theorem provers. The modalities within the AI Act and the logics suitable for their representation are discussed. For a selection of these logics, embeddings in HOL are created, which are then used to encode sample paragraphs. Initial experiments evaluate the suitability of these embeddings for automated reasoning, and highlight key challenges on the way to more robust reasoning capabilities.