原型验证系统（PVS）

检查过程中的最重要环节就是确保表格的完整性和一致性。为此，我们必须非常小心地验证各个定理的正确性。因此，选择一个优秀的定理证明系统是非常重要的。一个优秀的定理证明系统必须满足以下要求，才能被视为合格的定理证明系统：
 

• 必须具备处理与各种类型的数据进行交互的能力。
   
• 必须采用比其他方式更简单的表述方式来撰写。
   
• 必须自动进行验证。
   

为什么选择原型验证系统（PVS）呢？ 
PVS通常是一种规范语言，它与各种支持工具以及自动定理证明器相结合使用。 该软件自1993年起在加利福尼亚州门洛帕克的SRI国际大学的计算机科学实验室中开发出来。 实际上，它本质上是一种研究原型。随着我们开发出或应用了新的功能，该原型也会不断发展和改进。同时，在实际使用过程中，各种新的需求也会逐渐显现出来。 PVS规范语言通常基于传统的、带有类型标注的高阶逻辑体系。 这种规范语言被用来定义各种理论库。
原型验证系统（PVS）此外，它还包含了类型检查器、内置的理论以及用于验证的定理证明工具。因此，不同的应用程序都使用PVS来为系统的属性提供形式化验证支持。PVS的定理证明器实际上是一组基本推理规则以及高级的证明策略的集合。它可以在序列计算框架中交互式地使用。以下是选择PVS而非其他工具时需要考虑的一些重要因素：
 

• PVS能够自动生成与表格规范的有效性和一致性相关的各种定理。在PVS中，这些定理可以通过不同类型的构造器来轻松地被构建出来。
   
• PVS通常可以自动进行验证。通过这种验证方式，PVS能够轻松验证与完整性和一致性相关的各种定理。
   
• 此外，该方法还利用了经典逻辑和全函数理论。另一方面，它还能提供谓词和依赖类型，这些类型有助于限制那些原本属于部分函数的范畴的内容。
   
• 在创建类型检查条件时，该工具还会对理论内容进行解析和类型检查。
   
• 此外，该系统还会生成相应的文档，即用PostScript、HTML等格式编写的理论和证明内容。
   

PVS证明命令： 
PVS通常包含大量的命令。这些命令也被称为“规则”。下面列出了其中一些命令：
 

1. 控制指令： 
   该命令是控制和处理证明执行以及证明树遍历所必需的。
    
2. 结构指挥： 
   该命令是实施缩略规则以及隐藏那些在序列中并不被使用的公式所必需的。
    
3. 命题命令： 
   该命令是实施推理规则的必要条件，它不仅适用于连接词，也适用于复杂的运算符以及“cut”操作。
    
4. 量词命令： 
   该命令是实施量词推理规则所必需的。
    
5. 平等命令： 
   除了一些基本的序列计算规则之外，还需要使用这个命令来实施不同的推理规则。此外，还需要一些关于相等性、记录、元组等相关的规则。
    
6. 战略指挥： 
   该命令用于应用所有预先定义好的规则序列。
    
7. 定义与引理处理命令： 
   此命令是调用和应用引理以及定义所必需的。