"教"电脑怎么办？

Question

问题是教电脑做补充.计算机具有数字知识:他"知道"在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是添加数量的大小.

这个项目有什么科学价值吗？有没有可以做这些事情的程序？

Answer 1

那些不理解算术的自动定理证明符合你的建议:他们试图在每次需要时从定义中重新发明它.结果？它不能很好地工作.您可以通过提供关于算术的更高级别的一般事实来帮助这些证明者(或者作为公理,或者如果你是严格的,因为引理是单独证明的).示例:关联性,交换性,...

它仍然不能很好地工作.似乎有一个更直观明显的事实是你需要为工具提供你感兴趣的特定证据.例如,x> y => x> = y,z是奇数或偶数,属性就是这样...

为了弥补这个问题,一些自动定理证明器在内部处理算术.在这种情况下,结果更好.简化和替代是这种证明的两个例子.