Autarkic computations in formal proofs
Autarkic computations in formal proofs
复制标题
DOI：
10.1023/a:1015761529444
复制
发表时间：
2002-04-01
期刊：
影响因子：
--
通讯作者：
Barendsen, E
中科院分区：
文献类型：
--
作者：
Barendregt, H;Barendsen, E
数学和计算机科学中的形式证明正在被研究，因为这些对象可以通过一个非常简单的计算机程序来验证。一个重要的开放问题是，这些形式化的证明是否可以用不比用乳胶写一篇数学论文大得多的努力来生成。现代的证明开发系统使得推理的形式化相对容易。然而，以这种方式形式化计算，结果可以用于形式证明不是立即的。在本文中，我们展示了如何在Peano算术的背景下获得Prime（61）或在环的背景下获得（x +1）（x +1）=x（2）+2x+1等陈述的形式证明。我们希望该方法将有助于弥合计算机代数的有效系统和证明发展的可靠系统之间的差距。
Formal proofs in mathematics and computer science are being studied because these objects can be verified by a very simple computer program. An important open problem is whether these formal proofs can be generated with an effort not much greater than writing a mathematical paper in, say, LATEX. Modern systems for proof development make the formalization of reasoning relatively easy. However, formalizing computations in such a manner that the results can be used in formal proofs is not immediate. In this paper we show how to obtain formal proofs of statements such as Prime(61) in the context of Peano arithmetic or (x+1)(x+1)=x(2)+2x+1 in the context of rings. We hope that the method will help bridge the gap between the efficient systems of computer algebra and the reliable systems of proof development.