NASALib 是一项跨越 30 多年的持续合作成果，旨在协助 NASA 赞助的定理证明相关研究 (https://shemesh.larc.nasa.gov/fm/pvs/)。它由一系列用原型验证系统 (PVS) 编写的正式开发（即库）组成，由 SRI、NASA、NIA 和 PVS 社区贡献，并由 LaRC 的正式方法团队维护。
NASALib 当前版本为 7.1.2 (2023/09/01)，需要 PVS 7.1。
目前，NASALib由62个顶级库组成，总共包含约38K个经过验证的公式。
| 图书馆 | 描述 |
|---|---|
| 符合 | 空中交通冲突检测和解决算法分析框架 |
| 仿射_arith | 仿射算术的形式化和评估具有区间域变量的多项式函数的策略 |
| 代数 | 群、幺半群、环等 |
| 分析 | 实分析、极限、连续性、导数、积分 |
| ASP | 答案集编程的指称语义 |
| 航空 | 支持航空相关形式化的定义和属性 |
| 伯恩斯坦 | 多元伯恩斯坦多项式的形式化 |
| CCG | 多样化终止标准的形式化 |
| 复杂的 | 复数 |
| 复杂的替代品 | 复数的替代形式化 |
| 复杂的整合 | 复杂的集成 |
| 协同结构 | 定义为余代数数据类型的可数长度序列 |
| 有向图 | 有向图：电路、最大子树、路径、DAG |
| dL | 微分动态逻辑 |
| 精确实数 | 精确的实数算术，包括三角函数 |
| 例子 | NASALib提供的功能的应用示例 |
| 扩展_nnreal | 扩展非负实数 |
| 快速近似 | 标准数值函数的近似值 |
| 容错 | 容错协议 |
| 漂浮 | 浮点运算 |
| 图表 | 图论 |
| 间隔算术 | 区间算术和数值近似。包括用于计算数值近似值的自动化数值策略和用于检查简单量化实值公式的可满足性和有效性的区间。这一发展包括艾伦区间时序逻辑的形式化 |
| 整数 | 整数除法、gcd、mod、素因数分解、最小值、最大值 |
| 勒贝格 | 勒贝格积分与黎曼积分的联系 |
| 线性代数 | 线性代数 |
| 线段 | 二维线段 |
| 指数 | 对数、指数和双曲函数。 & 对数、指数和双曲函数的基本定义 |
| 零担运输 | 线性时态逻辑 |
| 矩阵 | MxN 矩阵的可执行规范。该库包括逆计算和基本矩阵运算，例如加法和乘法 |
| 测量整合 | 西格玛代数、测度、Fubini-Tonelli 引理 |
| 梅蒂·塔斯基 | 集成 MetiTarski（实值函数的自动定理证明器） |
| 度量空间 | 具有距离度量、连续性和一致连续性的域 |
| MV_分析 | 多元实数分析：范数、极限、连续性、导数、优化等。 |
| 多聚 | 多元多项式和半代数集。 |
| 名义上的 | 名义等式推理 |
| 数字 | 初等数论 |
| 常微分方程 | 常微分方程 |
| 订单 | 抽象阶、格、不动点 |
| 多边形 | 二维多边形 |
| 多边形合并 | 合并二维多边形而不产生孔 |
| 力量 | 广义幂函数（不含 ln/exp） |
| 可能性 | 概率论 |
| PVS0 | 基本可计算性概念的形式化 |
| pvsio_utils | PVSio 的补充，PVS 标准库，用于 PVS 规范的动画 |
| 雷亚尔 | 求和、sup、inf、实数开方、绝对值等 |
| 黎曼 | 黎曼积分 |
| 斯科特 | 斯科特拓扑 |
| 系列 | 幂级数、比较检验、比率检验、泰勒定理 |
| 组辅助 | 幂集、阶数、无限集上的基数。包括基于选择公理的功能和关系事实以及基于等价关系的细化关系 |
| 形状 | 2D 形状：三角形、平行四边形、矩形、圆弧 |
| 西格玛集 | 可数无限集的求和 |
| 排序 | 排序算法 |
| 结构 | 有界数组、有限序列、包和其他几种结构 |
| 斯图姆 | 单变量多项式的 Sturm 定理的形式化。包括用于自动证明实数区间内单变量多项式关系的sturm策略和mono-poly |
| 塔斯基 | 单变量多项式塔斯基定理的形式化。包括用于自动证明实线上单变量多项式关系系统的策略 tarski |
| 拓扑结构 | 连续性、同胚、连通空间和紧空间、Borel 集/函数 |
| 三角函数 | 三角学：定义、恒等式、近似值 |
| TRS | 术语重写系统和罗宾逊统一算法 |
| TU_游戏 | 合作TU博弈 |
| 向量分析 | 向量函数的极限、连续性和导数 |
| 向量 | 2-D、3-D、4-D 和 n 维向量 |
| 尽管 | 编程语言的语义 While |
NASALib 还提供了一组可自动执行多项任务的脚本。
proveit (*) - 以批处理模式运行 PVSprovethem (*) - 在多个库上运行proveitpvsio (*) - 用于运行 PVSio 地面评估器的命令行实用程序。prove-all - 通过包装provethem来在 NASALib 中的每个库上proveit证明，以提供特定类型的运行。cleanbin-all - 从 PVS 库中清理.pvscontext和二进制文件。find-all - 在 PVS 库中搜索与给定正则表达式匹配的字符串。dependencygraph - 为当前目录中的库生成库依赖关系图。dependency-all - 生成当前文件夹中 PVS 库的依赖关系图。单击此处了解有关这些脚本的更多详细信息。
(*) 已包含在 PVS 7.1 发行版中。
NASALib (v7.0.1) 与 VSCode-PVS 完全兼容，VSCode-PVS 是基于 Visual Studio Code 的现代 PVS 图形界面。可以从 VSCode-PVS 安装最新版本的 NASALib。
对于 PVS 高级用户，可以从 GitHub 获取开发版本。要克隆开发版本，请在安装 PVS 7.0 的目录中键入以下命令。此后，该目录将被称为
$ git clone http://github.com/nasa/pvslib nasalib 上面的命令会将库的副本放入目录
库groups现已弃用。 group库已集成到algebra中。仍提供符号链接以实现向后兼容性，但不鼓励使用它。每次提到groups都应该用algebra代替。
库trig_fnd现已弃用。它仍然是为了向后兼容而提供的，但它应该被trig取代。新的库trig曾经是公理化的，现在是基础性的。然而，与trig_fnd相比，三角函数定义基于无穷级数，而不是积分。这一变化大大减少了涉及三角函数的理论的类型检查。从trig_fnd到trig的更改不会对您的正式开发产生重大影响，因为定义和引理的名称是相同的。然而，理论导入可能略有不同。
PVS 开发的TCASII 、 WellClear和DAIDALUS现已作为 GitHub WellClear 发行版的一部分提供。 PVS 开发PRECiSA现已作为 GitHub PRECiSA 发行版的一部分提供。 PVS 开发PolyCARP现已作为 GitHub PolyCARP 发行版的一部分提供。
以下说明假设 NASALib 位于目录
PVS_LIBRARY_PATH中如果不存在，则创建该变量并以此目录的路径作为唯一内容。让 shell 系统在启动时创建此变量通常非常有用。为此，根据您的 shell，您可能需要在启动脚本中添加以下行之一。对于 C shell（csh 或 tcsh），您可以在~/.cshrc中添加此行：
setenv PVS_LIBRARY_PATH " /nasalib " 对于 Borne shell（bash 或 sh），请在~/.bashrc或~/.profile中添加以下行：
export PVS_LIBRARY_PATH= " /nasalib " 如果您以前安装过 NASALib，请删除文件~/.pvs.lisp ，或者如果您在该文件中有特殊配置，请删除以下行
( load " /nasalib/pvs-patches.lisp " ) 最后进入
install-scripts命令将根据需要更新和安装 NASALib 脚本。
$ ./install-scripts旧版本的 NASALib 可从 http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library 获取。
NASALib 多年来的发展得益于许多人的贡献，其中包括：
如果我们错误地归因了 PVS 开发，或者您为 NASALib 做出了贡献，但您的名字未包含在此处，请告知我们。
如果您想做出贡献，请阅读本指南。
NASALib 是正式规范的集合，其中大部分已在公共领域公开多年。 NASA LaRC 的形式方法团队仍然保持着这些发展。对于形式化方法团队最初进行的开发，这些开发被认为是不构成软件的基础研究。其他人做出的贡献可能具有特定的许可证，这些许可证列在每个目录的top.pvs文件中。如有疑问，请联系每个贡献的开发人员，这些开发人员也列在该文件中。
PVS 补丁包含在pvs-patches目录中，是 PVS 源代码的一部分，并且由 PVS 开源许可证涵盖。
一些证明策略需要第三方研究工具，例如 MetiTarski 和 Z3。为了方便起见，它们经过作者的许可包含在这个存储库中。这些工具的许可证也包含在适当的情况下。
好好享受。
LaRC 的形式化方法团队
塞萨尔·穆尼奥斯·马里亚诺·莫斯卡托
