问数学归纳法的自动定理证明
EN

Stack Overflow用户

提问于 2016-11-14 07:39:24

回答 1查看 85关注 0票数 0

如果有一种方法可以实现数学归纳的证明程序，它看起来会是什么样子？如果不可能，原因何在？

我想到了一种方法，在这种方法中，你可以指定基本公理和规则作为输入，并将其限制在基本和和方程的问题上。

一般来说，数学证明也是这样吗？

发布于 2016-11-14 08:20:16

我将把答案限制在自然数的归纳上。

假设S(n)是您想要通过对所有n进行归纳来证明的语句。然后程序将需要检查：S(0)和S(n) => S(n+1)。

第一部分就像证明一些陈述一样困难，第二部分是关于证明两个这样的陈述的等价性。这意味着，即使第一部分不难，第二部分可能是NP-hard (据我所知)。所以，是的，可以实现一个校验器(只需要检查一条语句和两条语句的等价性)，但我认为你不能保证它会终止。

票数 0

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/40580039

复制

相似问题

问数学归纳法的自动定理证明EN