Teaching proofs is a crucial component of any undergraduate-level program that covers formal reasoning. We have developed a calculational reasoning format and refined it over several years of teaching a freshman-level course, "Logic and Computation", to thousands of undergraduate students. In our companion paper, we presented our calculational proof format, gave an overview of the calculational proof checker (CPC) tool that we developed to help users write and validate proofs, described some of the technical and implementation details of CPC and provided several publicly available proofs written using our format. In this paper, we dive deeper into the implementation details of CPC, highlighting how proof validation works, which helps us argue that our proof checking process is sound.

翻译：教学证明是任何涉及形式推理的本科课程中的关键组成部分。我们开发了一种计算化推理格式，并通过多年教授面向数千名本科生的新生课程“逻辑与计算”不断加以完善。在配套论文中，我们介绍了计算化证明格式，概述了为帮助用户编写和验证证明而开发的计算化证明检查器（CPC）工具，描述了CPC的一些技术实现细节，并提供了数个使用该格式编写的公开可用证明。在本文中，我们将深入探讨CPC的实现细节，重点阐述证明验证的工作原理，这有助于论证我们的证明检查过程是可靠的。