Using an interactive theorem prover to reason about programs involves a sequence of interactions where the user challenges the theorem prover with conjectures. Invariably, many of the conjectures posed are in fact false, and users often spend considerable effort examining the theorem prover's output before realizing this. We present a synergistic integration of testing with theorem proving, implemented in the ACL2 Sedan (ACL2s), for automatically generating concrete counterexamples. Our method uses the full power of the theorem prover and associated libraries to simplify conjectures; this simplification can transform conjectures for which finding counterexamples is hard into conjectures where finding counterexamples is trivial. In fact, our approach even leads to better theorem proving, e.g. if testing shows that a generalization step leads to a false conjecture, we force the theorem prover to backtrack, allowing it to pursue more fruitful options that may yield a proof. The focus of the paper is on the engineering of a synergistic integration of testing with interactive theorem proving; this includes extending ACL2 with new functionality that we expect to be of general interest. We also discuss our experience in using ACL2s to teach freshman students how to reason about their programs.
Proof Artifact Co-training for Theorem Proving with Language Models
University of Pittsburgh（匹兹堡大学）；OpenAI；IBM Research（IBM研究院）；Google Research（谷歌研究院）；Stanford University（斯坦福大学）；Carnegie Mellon University（卡内基梅隆大学）；CIBO Technologies（CIBO科技）；University of Toronto（多伦多大学）；University of Cambridge（剑桥大学）
Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover for ProB
Faculty of Mathematics；Natural Science, Institute of Computer Science, Heinrich Heine University Düsseldorf, Universit\" a tsstr. 1, D-40225 D\" u sseldorf
Michael John Caldwell Gordon (FRS 1994), 28 February 1948 -- 22 August 2017
Michael Gordon是交互式定理证明和硬件验证领域的先驱。在20世纪70年代，他的愿景是正式验证系统设计，使用数学和逻辑证明其正确性。他在现实世界的计算机设计中展示了他的想法。他的学生将工作扩展到不同的领域，如浮点算法的验证，概率算法的验证和源代码的验证翻译，以纠正机器码。他当选为英国皇家学会于1994年，他继续生产杰出的研究，直到退休。他的成就包括他在爱丁堡大学的工作，帮助创建爱丁堡LCF，第一个交互式定理证明器，以及ML家族的函数式程序设计语言。他采用高阶逻辑作为验证的一般形式，表明它可以指定从门级到处理器级的硬件设计。它被证明是计算机科学和数学中许多问题的理想形式。他的工具和技术在形式化验证领域产生了巨大的影响。
