Masterarbeit, Otto-Friedrich-Universität Bamberg, 2024

This work investigates the feasibility and methodology of representing the European Union’s AI Act in Higher-Order Logic to facilitate automated ethical reasoning. The AI Act and its modalities are thoroughly analyzed, and existing embeddings of Standard Deontic Logic and Dyadic Deontic Logic are employed to represent a selection of these modalities, specifically Obligations and Contrary-to-Duty Obligations, in Isabelle/HOL. To capture Agency and Agentive Obligations, embeddings of Temporal Deontic STIT logic and variants of DDL are introduced. The effectiveness and limitations of different embeddings are evaluated by formalizing example sections of the AI Act in the embedded logics and utilizing the automated theorem provers, satisfiability modulo theories solvers, and model finders available in Isabelle/HOL. The results provide valuable insights into the challenges of automated legal reasoning in HOL in a complex context, highlighting the strengths and limitations of current theorem-proving tools.