ACM通信
评论文章
机械数学家
图源:Martin Capek
在20世纪60年代，研究人员梦想着自动定理证明足够强大，可以对以前没有人能够证明的猜想提出冗长的证明。一些人甚至认为这些“机械数学家”最终将取代有血有肉的数学家。然而，在几十年的时间里，自动证明仍然太弱，无法帮助数学家，更不用说取代数学家了。相反，数学家转向了计算机代数系统，它对证明的帮助不如对计算的帮助，自动证明转向了其他应用领域。这些领域包括硬件和软件验证，直接或通过交互式验证平台(例如，Atelier B, Dafny, F*， Frama-C, SPARK 2014, spec#， VCC, Why3)。此外，自动证明程序被用作通用证明助手(例如ACL2、Coq、HOL、Isabelle、Lean、Mizar、PVS)的后端。随着数学家们慢慢接受证明助手，自动证明终于对他们有用了，可以执行直接但乏味的证明任务。
关键的见解
作为初等数学中的一个简单例子，考虑这个公式
逻辑符号∧和⇒都表示“和”和“和”，gcd是最大公约数，|是两个数之间的“除”关系(例如:d|ab意味着ab能被d)．让我们来看看一个特殊的情况:如果一个= 12,b= 35，和d= 5，我们有一个“= 1,b”= 5，确实如此一个b= 5除d= 5，反之亦然。数学家们可以很容易地看出这个公式在一般情况下是成立的，但是为一个证明助手写一个具有可接受的细节水平的正式证明很容易需要15或30分钟。相比之下，自动定理证明程序可以在几秒钟内证明这些公式。
没有找到条目