Logical Modalities within the European AI Act: An Analysis
This work addresses the problem of formalizing legal AI regulations for automated reasoning, which is incremental as it applies existing logical methods to a new domain.
The paper analyzes the European AI Act to prepare its formal representation using logical modalities, specifically through embeddings in Higher-Order Logic within the LogiKEy framework, and conducts initial experiments to evaluate their suitability for automated reasoning while identifying key challenges.
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.