The Inconsistency in Gödel's Ontological Argument: A Success Story for AI in Metaphysics
The Inconsistency in Gödel's Ontological Argument: A Success Story for AI in Metaphysics
复制标题
哥德尔本体论论证的不一致：人工智能在形而上学中的成功故事
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
B. W. Paleo
中科院分区：
文献类型：
--
作者：
Christoph Benzmüller;B. W. Paleo
本文讨论了哥德尔本体论论证中发现的不一致作为人工智能的成功故事。尽管自 1970 年代初哥德尔手稿出现以来，该论证很受欢迎，但该论证中使用的公理的不一致一直未被注意到，直到 2013 年，它被高阶定理证明器 LEO-II 自动检测到。理解和验证证明者生成的反驳结果是一项耗时的任务。正如这里所报道的，它的完成需要在 Isabelle 证明助手中重建反驳，并且它还带来了一种新颖且更有效的方法来自动化具有通用可访问性关系的高阶模态逻辑 S5。此外，针对所使用的逻辑嵌入技术开发了改进的句法隐藏，使得反驳能够以人性化的方式呈现，适合高阶定理证明技术方面的非专家。这使我们距离哲学家更广泛地采用基于逻辑的人工智能工具又近了一步。
This paper discusses the discovery of the inconsistency in Godel's ontological argument as a success story for artificial intelligence. Despite the popularity of the argument since the appearance of Godel's manuscript in the early 1970's, the inconsistency of the axioms used in the argument remained unnoticed until 2013, when it was detected automatically by the higher-order theorem prover LEO-II. Understanding and verifying the refutation generated by the prover turned out to be a time-consuming task. Its completion, as reported here, required the reconstruction of the refutation in the Isabelle proof assistant, and it also led to a novel and more efficient way of automating higher-order modal logic S5 with a universal accessibility relation. Furthermore, the development of an improved syntactical hiding for the utilized logic embedding technique allows the refutation to be presented in a human-friendly way, suitable for non-experts in the technicalities of higher-order theorem proving. This brings us a step closer to wider adoption of logic-based artificial intelligence tools by philosophers.
作为形而上学的模态逻辑
DOI：
--
发表时间：
2013
期刊：
--
影响因子：
--
作者：
Williamson T
通讯作者：
Williamson T
使用 SMT 求解器扩展 Sledgehammer
DOI：
10.1007/s10817-013-9278-5
发表时间：
2013
期刊：
Journal of Automated Reasoning
影响因子：
--
作者：
Jasmin Christian Blanchette;Sascha Böhme;Lawrence C. Paulson
通讯作者：
Lawrence C. Paulson