2025/01/31 by Lara Lawniczak, Christoph Benzmüller, Lawniczak, Lara +1
Computer Science · Social Sciences · #68T01 68T27 68T30 03Axx 03B16 03B35 03B45 03B60 03B70 #Artificial Intelligence (cs.AI) #Computers and Society (cs.CY) #Digitalization, Law, and Regulation #FOS: Computer and information sciences #I.2.0 #I.2.3 #I.2.4 #J.1 #Law, AI, and Intellectual Property #Logic in Computer Science (cs.LO)
paper · pdf · doi:10.48550/arxiv.2501.19112
openalex publication_date 2025/01/31 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.