Re: 高性能CPU研发能够离开定理证明器吗

发信人: lingcore (), 信区: CSArch
标  题: Re: 高性能CPU研发能够离开定理证明器吗
发信站: 水木社区 (Wed Feb  2 00:46:47 2011), 站内

形式验证可以分成两类。一类是全部依靠自动工具的，另一类是人机交互证明。我们讲的是第二类，并把它们称为定理证明器，以示同第一类的区别。

第一类工具不能出来大规模的验证问题，第二类不受问题规模的限制，因为它通过人机交互的方式进行证明。人可以把大问题分解成小问题，大定理的证明化解成一组小的引理的证明，可以使用归纳法。可以开发各种证明策略，甚至去扩展定理证明器的功能。

用交互式证明器做验证，同数学家证明定理相似。区别在于，在使用证明器时可以调用一些程序去证明某些小定理，但另一方面，证明过程比数学家要更为细致。对许多数学家认为“显然”的东西，在计算机中需要开发出一套专门的数学理论。

交互式证明同软件开发也有相似性。开发一个证明相当于写了一个大软件。在INTEL中，人工写的证明策略的长度超过VERILOG代码的长度。