# Logical Modalities within the European AI Act: An Analysis

arXiv: https://arxiv.org/abs/2501.19112 · HTML: https://mlsanity.com/paper/2501.19112/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 3 of its 41 references that are in the map.
- First posted on arXiv 31 Jan 2025.

## Builds on (most cited first, 3 of 3)

- [Normative Conditional Reasoning as a Fragment of HOL](https://mlsanity.com/paper/2308.10686/) (2023)
- [A Neutral Temporal Deontic STIT Logic](https://mlsanity.com/paper/1907.03265/) (2019)
- [First Experiments with a Flexible Infrastructure for Normative Reasoning](https://mlsanity.com/paper/1804.02929/) (2018)

## Built on by (most cited first, 2 of 2)

- [Faithful Logic Embeddings in HOL -- Deep and Shallow](https://mlsanity.com/paper/2502.19311/) (2025)
- [Mathematical Proof Assistants for Teaching Logic: The LogiKEy Methodology](https://mlsanity.com/paper/2610.08214/) (2026)

## Abstract (arXiv)

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.