不同定理证明系统（TPS）

定理证明系统(TPS)也称为自动证明系统。适用于实时系统设计和验证的定理证明通常使用几种定义和不同的定理，从根本上帮助设计，实现，验证和验证需求。这些证明方法还可以提供更高级别的软件要求规范以及详细的实现说明。然后可以仅根据规范检查这些实现，以确保其正确与否。自动定理证明通常集中于并旨在“识别”或“寻找”方面。

不同的定理证明系统：
有很多很好的定理证明者系统，并且与我们的工作有关。其中一些如下：

1. 交互式数学证明系统(IMPS)：
   IMPS的主要目的只是为传统的数学推理技术提供机械化的支持。它也提供了大的原始推理步骤，只是为了方便人类对演绎过程的控制和对结果证明的人类理解。它也是PVS的非常强大的替代品，并且可能还需要进行软件检查。 IMPS的逻辑还允许部分功能和通常未定义的术语。
2. 伊莎贝尔：
   Isabelle基本上是泛型证明助手或泛型定理证明系统。它通常提供一个框架，在其中可以通过简单地指定其逻辑和推理规则来添加各种逻辑。它最初是由剑桥大学和慕尼黑工业大学开发的。它还提供了元逻辑，也称为弱类型理论，可能需要对诸如一阶逻辑(FOL)，高阶逻辑(HOL)等对象逻辑进行编码。它也被视为实现各种逻辑的工具逻辑，以及定义和检查异类证明系统。
3. 高阶逻辑定理证明系统：
   HOL定理证明器基本上是通用的，并且是最广泛使用的计算机程序，用于构造程序规范和高阶逻辑的形式证明。它也可以用作通用定理证明研究的开放平台，也可以用作形式化数学的平台。它还支持各个领域的推理，以及硬件设计和验证，有关实时系统的证明，编译器验证，程序正确性以及程序优化。如今，基本上有四种不同的HOL系统可以处理，维护和开发，即HOL4源自HOL88系统，HOL Light，ProofPower和HOL Zero。它也用作定理证明研究的平台。
4. 原型验证系统(PVS)：
   PVS通常为正式的规范和验证提供机械化的支持。它通常是用于简单编写规范并构造证明的原型系统。 PVS已完全实施并免费提供。它还包括许多预定义的理论，定理证明，不同的实用程序和文档。它的规范通常组织成参数化理论。它还提供了极富表现力和自然的规格。
5. 定理证明系统(TPS)：
   它基本上是作为证明高阶逻辑和一阶逻辑定理的方法的研究计划的一部分而开发的。 TPS可能不是我们的工作，而是PVS，但PVS更易于访问。它还包含公式编辑器，该编辑器简单地促进了从TPS已知的其他公式中构造新公式。