ACL2s中的计算证明
摘要：教大学生如何撰写严密的证明是引入形式推理课程的关键目标。经过几年的发展，我们开发了一种可机械检查的计算推理风格，我们在东北大学的“逻辑与计算”课程中使用这种风格教授了1000多名大一学生如何推理计算。我们受到Dijkstra的影响，他提倡使用计算证明，并写道：“计算证明几乎总是比所有非正式方法更有效，...，计算证明的设计似乎比发现非正式证明的艺术更易教。”我们的计算证明检查器已集成到ACL2s中，并可作为Eclipse IDE插件、Web界面和独立工具提供。它自动检查证明的正确性并提供有用的反馈。我们描述了检查器的架构、证明格式、底层算法、正确性，并提供了从我们的本科课程和Dijkstra的证明中使用的示例。我们还描述了使用证明检查器教授本科生如何形式地推理计算的经验。
作者：Andrew T. Walter, Ankit Kumar, Panagiotis Manolios
论文ID：2307.12224
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-25