论文标题
迈向哥德尔的两个不完整定理的机器发现的证据
Towards Concise, Machine-discovered Proofs of Gödel's Two Incompleteness Theorems
论文作者
论文摘要
将AI的最新进展应用于自动推理的兴趣越来越大，因为它可能在一阶，二阶甚至元记录的形式主义方面提供了有用的启发式方法。为了促进这项研究，我们提出了MATR，这是一个新的自动定理框架，该框架明确设计地旨在轻松适应异常逻辑或整合新的推理过程。 MATR是形式主义 - 敏捷，高度模块化和程序员友好的。我们解释了MATR的高级设计以及其实施的一些细节。为了展示MATR的效用，我们描述了一种适合证明Gödel的不完整定理的形式化的金属材料，并报告了我们使用MATR中的Metalogic的进度来报告半自主的第一和第二不完整定理的证明。
There is an increasing interest in applying recent advances in AI to automated reasoning, as it may provide useful heuristics in reasoning over formalisms in first-order, second-order, or even meta-logics. To facilitate this research, we present MATR, a new framework for automated theorem proving explicitly designed to easily adapt to unusual logics or integrate new reasoning processes. MATR is formalism-agnostic, highly modular, and programmer-friendly. We explain the high-level design of MATR as well as some details of its implementation. To demonstrate MATR's utility, we then describe a formalized metalogic suitable for proofs of Gödel's Incompleteness Theorems, and report on our progress using our metalogic in MATR to semi-autonomously generate proofs of both the First and Second Incompleteness Theorems.
