Tinycals：细粒度战术评估革新交互式定理证明

本文主要探讨了理论计算机科学中的一个重要议题，即交互式定理证明方法，特别是在过程证明语言和LCF战术的背景下。LCF战术通常被高级证明助手如NuPRL、Isabelle、Coq和Matita等采用，这些系统的核心在于用户通过文本脚本记录一系列战术来推动证明过程，战术被视为策略的基本单元。然而，这些系统的设计往往受限于粗粒度的战术评估，导致用户界面与证明策略之间的交互存在一些问题。 文章指出，当前的交互范例，尤其是那些基于声明性证明语言（如Mizar）与过程证明核心并存的系统（如Isabelle/Isar），虽然在设计上受到CtCoq早期工作的启发，但其用户界面与证明逻辑的结合并不完美。例如，Mizar采用声明性证明，而其他系统如NuPRL和Coq则侧重于过程证明，这种差异可能导致用户体验上的不便。 作者提出了一种名为Tinycals的替代方案，它是LCF战术的一个子集，主张通过更精细的战术评估粒度来改善用户界面。Tinycals旨在解决当前系统中用户与战术交互时面临的挑战，比如战术评估效率低下或复杂性过高等问题。文章还阐述了Tinycals的正式操作语义以及在Matita证明助手中的实现情况。 Tinycals的引入旨在提供一个更流畅、直观的交互体验，使用户能够更加有效地管理战术组合，从而提高定理证明的效率和可读性。此外，作者的工作也关注了小步语义（step-by-step semantics）的概念，这是一种注重证明过程逐步推进的方法，有助于用户跟踪证明的每一步，并增强证明的透明度。 本文对交互式定理证明的现有实践进行了深入分析，并提出了Tinycals作为一种改进工具，以提升用户界面与战术策略的有效交互，对于理论计算机科学领域的证明辅助工具的发展具有重要意义。