arXiv:2501.19112v2 宣告类型: 更换 摘要：本文从逻辑模态的角度对《欧洲人工智能法案》进行了全面分析，旨在为其正式表示做准备，例如在逻辑多元化的知识工程框架和方法（LogiKEy）中。LogiKEy 基于形式方法开发了基于逻辑的计算工具，采用高级逻辑（HOL）作为统一的元逻辑，通过浅层语义嵌入来整合多种逻辑。这种整合借助了 Isabelle/HOL，这是一个配备了多种自动定理证明器的证明助手工具。文中讨论了《人工智能法案》中的模态及其表示所适用的逻辑。对于这些逻辑中的一小部分，创建了在 HOL 中的嵌入，然后使用这些嵌入对样本段落进行编码。初步实验评估了这些嵌入在自动推理方面的适用性，并指出了通往更稳健推理能力过程中的关键挑战。