交互式定理证明：战术选择与重用技术

交互式定理证明是理论计算机科学领域的重要研究方向，它关注如何通过自动化的证明搜索来辅助人类专家在复杂逻辑系统中验证定理。在《理论计算机科学电子札记》58卷第2期（2001年）的一篇文章中，作者阿克塞尔·谢勒、塞尔日·奥特谢尔和迪特·哈特探讨了策略定理证明的战术层面，这是一种更为精细的操作层次，它超越了简单的规则顺序应用。 传统的交互式定理证明中，用户主要负责决定在高层面上采用哪种策略，而战术的运用则相对有限，用户不能在策略执行过程中进行干预。然而，本文提出了一项创新技术，旨在增强战术定理证明的灵活性和效率。该技术允许用户在战术的执行过程中介入，比如明确选择操作点，从而避免陷入无效的路径，即所谓的死胡同。这一技术的关键在于战术的有效重放，它能够复现战术的执行过程，而无需重新进行可能耗时的原始搜索。 战术不仅包含了基本的控制结构，如迭代、条件分支，还可能包含策略上的不确定性选择，这使得战术能够处理更为复杂的证明任务。通过将目标分解为子目标，策略可以递归地调用其他策略，形成一个动态的策略调用树，反映了策略在特定目标上的执行路径。这个结构与静态的策略调用图相辅相成，展示了策略如何通过搜索过程逐步逼近证明。 值得注意的是，由于策略的执行涉及到搜索和不确定性，策略调用树中的部分可能会因为搜索的失败而改变，这增加了证明过程的动态性和探索性。这项技术革新了交互式定理证明的方式，使得用户能更有效地指导和利用策略，从而提升证明效率和证明质量。