Theorem Prover

定义 Definition

theorem prover（定理证明器）：一种用于自动或半自动检验、构造或辅助构造数学定理与逻辑命题证明的软件系统（或工具）。常见于形式化验证、程序正确性证明与逻辑研究中。（也常泛指“证明助理/证明器”这一类工具。）

发音 Pronunciation

/ˈθiːərəm ˈpruːvər/

例句 Examples

The theorem prover confirmed that the proof was valid.
定理证明器确认该证明是有效的。

Using a theorem prover, researchers can formally verify that a cryptographic protocol satisfies its security properties.
借助定理证明器，研究人员可以形式化验证某个密码协议满足其安全性质。

词源 Etymology

theorem 源自希腊语 theōrēma（“可供观照之物、命题”），经拉丁语进入英语；prover 来自 prove（证明），其词根与拉丁语 probare（检验、证明）有关。合起来直译即“用于证明定理的工具/证明者”，在计算机科学语境中转指软件系统。

相关词 Related Words

• Proof Assistant
• Formal Verification
• Automated Reasoning
• Model Checker
• Logic
• Inference
• Soundness
• Completeness

文学与著作 Literary Works

• Software Foundations（Benjamin C. Pierce 等）：在介绍 Coq 时频繁使用并讨论 “theorem prover / proof assistant”。
• Interactive Theorem Proving and Program Development（Yves Bertot, Pierre Castéran）：以 Coq 为核心，系统讨论交互式定理证明器。
• Handbook of Automated Reasoning（Robinson, Voronkov 编）：多处出现 “theorem prover(s)” ，讨论自动推理与证明系统。
• The Calculus of Constructions（Thierry Coquand, Gérard Huet 等相关论文与文献）：讨论奠基于定理证明器/证明助理的类型论框架。