TLA +证明
TLA+ Proofs
摘要：
TLA+是一种基于标准集合论和时态逻辑的规约语言，具有用于分层证明的构造。我们描述了如何编写TLA+证明并使用TLAPS（TLA+证明系统）进行检查。我们使用彼得森的互斥算法作为一个简单的例子来描述TLAPS的功能，并展示它和TLAPS（TLA+的IDE）如何帮助用户管理大型，复杂的证明。
英文摘要：
TLA+ is a specification language based on standard set theory and temporal logic that has constructs for hierarchical proofs. We describe how to write TLA+ proofs and check them with TLAPS, the TLA+ Proof System. We use Peterson's mutual exclusion algorithm as a simple example to describe the features of TLAPS and show how it and the Toolbox (an IDE for TLA+) help users to manage large, complex proofs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
