检查过程的主要重要部分是检查表的完整性和一致性。为此，我们在证明定理时需要非常小心。因此，选择好的定理证明者系统是非常重要的任务。一个定理证明者系统必须满足以下几点才能被认为是好的定理证明者系统：
- 必须具有足够的能力来处理部分函数和各种类型的数据并与之交互。
- 与其他产品相比，必须以简单的方式制定。
- 必须自动验证。
为什么选择原型验证系统(PVS)?
PVS通常是规范语言，与支持工具和自动定理证明器集成在一起。它于1993年在位于加利福尼亚州门洛帕克(Menlo Park)的SRI International的计算机科学实验室开发。它基本上是研究原型，因为当我们创建或应用新功能时它会不断发展和改进，而实际使用中的压力会暴露所有新要求。 PVS规范语言通常基于经典的类型化高阶逻辑。需要指定语言来指定理论库。
原型验证系统(PVS)还包括用于验证的类型检查器，内置理论和定理证明。因此，不同的应用程序仅使用PVS为其系统属性提供正式的验证支持。 PVS定理证明者基本上是基本推理规则和高级证明策略的集合。它在后续演算框架之间以交互方式应用。以下是一些在选择PVS而非其他方面被认为重要的原因：
- PVS会自动生成与表格规范检查中的完整性和一致性相关的不同定理。在PVS中，借助不同类型的构造函数可以轻松地制定定理。
- PVS通常会自动得到验证。通过此验证，PVS可以简单地验证与完整性和一致性相关的各种定理。
- 它还需要经典逻辑和全部功能的帮助。另一方面，它还提供谓词和从属类型，可用于约束原本属于部分函数的域。
- 它还在创建类型检查条件(TCC)时对理论进行解析和类型检查。
- 它还会生成文档，例如PostScript，HTML等的理论和证明。
PVS Prover命令：
PVS通常包含大量命令。这些命令也称为规则。其中一些如下：
- 控制命令：
需要此命令来控制和处理证明执行和证明树浏览。 - 结构指令：
实施收缩规则和隐藏未按顺序使用的公式时，需要此命令。 - 命题命令：
对于复杂的运算符和剪切而言，仅此一个谓词就需要该命令来实现推理规则。 - 量词命令：
需要此命令来实现量词的推理规则。 - 平等命令：
除了一些基本的顺序演算之外，还需要此命令来实现不同的推理规则，以及用于相等性，记录，元组等的一些规则。 - 策略命令：
该命令用于应用所有预定义的规则序列。 - 定义和引理处理命令：
需要使用此命令来调用和应用引理以及定义。