<分区>
问题是教计算机做加法。 计算机具有数字知识:他“知道”1 之后是 2，2 之后是 3，依此类推。有了那台数据计算机就可以很容易地得到下一个数字。
接下来，计算机知道x+0=x 和x+(y+1)=(x+1)+y。这个公理让计算机做加法。例如，要将 5 和 3 相加，计算机会执行以下操作: 5+3 = 5+(2+1) = (5+1)+2 = 6+2 = 6+(1+1) = (6 +1)+1 = 7+1 = 8。
但是以这种方式添加数字太长了。问题是开发可以使用数学和逻辑规则改进这种加法方式的程序。目标应该是加法必须在 O(log(N)) 时间内执行，而不是 O(N) 时间，N 是相加数的大小。
这个程序有科学值(value)吗？有什么程序可以做这样的事情吗？
最佳答案
那些automatic theorem provers那些不懂算术的人按照你的建议去做:他们每次需要时都试图根据定义重新发明它。结果？它不能很好地工作。你可以通过提供关于算术的更高层次的一般事实来帮助这些证明者(作为公理，或者如果你是严谨的，作为单独证明的引理)。示例:结合律、交换律……
它仍然不能很好地工作。似乎总是有一个更直观明显的事实，即您需要向工具提供您感兴趣的特定证明。例如，x>y => x>=y，z 要么是奇数要么是偶数，诸如此类的属性...
为了弥补这个问题，一些自动定理证明器在内部处理算术。在这种情况下，结果会更好。 Simplify 和 alt-ergo 是此类证明者的两个例子。
关于algorithm - "Teach"一台电脑如何做加法？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/1481082/