arXiv:2501.19112v1 宣告类型: 新 摘要：本文从逻辑模态的角度对欧洲AI法案进行了全面分析，旨在为其正式表示做准备，例如，在逻辑-多元知识工程框架和方法论（LogiKEy）内进行表示。LogiKEy 开发了基于形式方法的规范推理计算工具，采用高阶逻辑（HOL）作为统合元逻辑，通过浅层语义嵌入将不同的逻辑进行整合。这一整合过程由一种配有多种自动化定理证明器的证明助手工具Isabelle/HOL 支持。文中讨论了AI法案中的模态及其适合表示的逻辑。为这些逻辑中的一部分创建了HOL中的嵌入，并利用这些嵌入对样本段落进行编码。初始实验评估了这些嵌入对于自动化推理的适用性，并突出了通往更可靠的推理能力过程中的一些关键挑战。