Beluga 中元理论证明的半自动化

我们给出了证明助手 Beluga 背后逻辑核心的一个可靠且完备的聚焦演算，并概述了其作为 Beluga 交互式证明环境 Harpoon 中策略的实现。该聚焦演算旨在构造 Beluga 中上下文 LF 及其元逻辑的一致证明：一种带递归依赖类型的依赖类型一阶逻辑。所实现的策略旨在完成证明中直截了当的子情形，使用户仅关注证明中有趣的方面，将繁琐简单的情况留给 Beluga 的定理证明器。我们通过使用该策略简化简单类型 lambda 演算的弱头正规化的证明来展示我们工作的有效性。