NASALib は、NASA (https://shemesh.larc.nasa.gov/fm/pvs/) が後援する定理証明に関連する研究を支援するために、30 年以上にわたって継続的に行われている共同作業です。これは、プロトタイプ検証システム (PVS) で記述された正式な開発のコレクション (つまり、ライブラリ) で構成され、SRI、NASA、NIA、および PVS コミュニティによって提供され、LaRC の形式メソッド チームによって維持されます。
NASALib の現在のバージョンは 7.1.2 (2023/09/01) で、PVS 7.1 が必要です。
現在、NASALib は 62 のトップレベルライブラリで構成されており、合計で約 38,000 の実証済みの公式が含まれています。
| 図書館 | 説明 |
|---|---|
| アコード | 航空交通の衝突検出および解決アルゴリズムを分析するためのフレームワーク |
| アフィン_アリス | アフィン演算の形式化と区間領域の変数を使用した多項式関数を評価する戦略 |
| 代数 | 群、モノイド、環など |
| 分析 | 実際の解析、限界、連続性、導関数、積分 |
| ASP | 解答セットプログラミングの表示意味論 |
| 航空 | 航空関連の形式化の定義とプロパティをサポート |
| バーンスタイン | 多変量バーンスタイン多項式の形式化 |
| CCG | 多様な解雇基準の正式化 |
| 複雑な | 複素数 |
| complex_alt | 複素数の代替形式化 |
| 複合統合 | 複雑な統合 |
| 共構造 | 共代数データ型として定義された可算長のシーケンス |
| ダイグラフ | 有向グラフ: 回路、最大サブツリー、パス、DAG |
| dl | 差動ダイナミックロジック |
| 正確な実数 | 三角関数を含む正確な実数演算 |
| 例 | NASALibが提供する機能の応用例 |
| 拡張_nnreal | 拡張された非負の実数 |
| 速い_おおよそ | 標準数値関数の近似 |
| フォールトトレランス | フォールトトレランスプロトコル |
| フロート | 浮動小数点演算 |
| グラフ | グラフ理論 |
| 間隔値 | 区間演算と数値近似。数値近似を計算するための自動化された数値戦略と、単純に定量化された実数値式の充足可能性と妥当性をチェックするための間隔が含まれています。この開発には、アレン区間時相論理の形式化が含まれています |
| 整数 | 整数の除算、gcd、mod、素因数分解、最小値、最大値 |
| ルベーグ | リーマン積分に関連するルベーグ積分 |
| 線形代数 | 線形代数 |
| 線分 | 2次元の線分 |
| lnexp | 対数関数、指数関数、双曲線関数。 & 対数、指数関数、双曲線関数の基本的な定義 |
| LTL | 線形時相論理 |
| 行列 | MxN 行列の実行可能な仕様。このライブラリには、逆行列の計算や、加算や乗算などの基本的な行列演算が含まれています。 |
| 測定統合 | シグマ代数、測度、フビニ・トネリ補題 |
| メティタルスキー | 実数値関数の自動定理証明器である MetiTarski の統合 |
| メトリックスペース | 距離メトリック、連続性、均一連続性を持つドメイン |
| mv_分析 | 多変量実解析: 規範、限界、連続性、導関数、最適化など。 |
| マルチポリ | 多変量多項式と半代数集合。 |
| 名目上の | 名目等式推論 |
| 数字 | 初歩的な整数論 |
| ODE | 常微分方程式 |
| 注文 | 抽象的な順序、格子、固定点 |
| ポリゴン | 2次元ポリゴン |
| ポリゴンマージ | 穴を発生させずに 2 次元ポリゴンを結合 |
| 力 | 一般化べき乗関数 (ln/exp なし) |
| 確率 | 確率論 |
| PVS0 | 基本的な計算可能性の概念の定式化 |
| pvsio_utils | PVS 仕様のアニメーション用の PVS 標準ライブラリである PVSio への追加 |
| 実数 | 合計、sup、inf、実数の二乗、絶対値など |
| リーマン | リーマン積分 |
| スコット | スコットトポロジー |
| シリーズ | べき級数、比較検定、比検定、テイラーの定理 |
| セット_aux | 無限集合に対するべき乗集合、順序、カーディナリティ。選択公理に基づく機能的事実と関係的事実、および等価関係に基づく改良関係が含まれます。 |
| 形 | 2D 形状: 三角形、平行四辺形、長方形、円形セグメント |
| sigma_set | 可算無限集合の合計 |
| 並べ替え | 並べ替えアルゴリズム |
| 構造物 | 有界配列、有限シーケンス、バッグ、およびその他のいくつかの構造 |
| シュツルム | 一変量多項式に対するシュトルムの定理の形式化。実区間にわたる一変量多項式関係を自動的に証明するための戦略sturmおよびmono-polyが含まれています |
| タルスキ | 一変量多項式に対するタルスキーの定理の形式化。実数直線上の一変量多項式関係の系を自動的に証明するための戦略 tarski が含まれています |
| トポロジー | 連続性、準同型性、接続されたコンパクト空間、ボレル集合/関数 |
| 三角関数 | 三角法: 定義、恒等式、近似 |
| TRS | 用語書き換えシステムとロビンソン統一アルゴリズム |
| TU_ゲーム | 協力TUゲーム |
| ベクトル分析 | ベクトル関数の極限、連続性、導関数 |
| ベクトル | 2 次元、3 次元、4 次元、および n 次元ベクトル |
| その間 | プログラミング言語のセマンティクス |
NASALib は、いくつかのタスクを自動化するスクリプトのコレクションも提供します。
proveit (*) - PVS をバッチ モードで実行しますprovethem (*) - 複数のライブラリでproveitを実行しますpvsio (*) - PVSio 地上評価器を実行するコマンドライン ユーティリティ。prove-all - 特定の種類の実行を提供するために、 provethemラップすることにより、NASALib の各ライブラリでproveitを実行します。cleanbin-all - PVS ライブラリから.pvscontextおよびバイナリ ファイルを削除します。find-all - PVS ライブラリ内の指定された正規表現に一致する文字列を検索します。dependencygraph - 現在のディレクトリ内のライブラリのライブラリ依存関係グラフを生成します。dependency-all - 現在のフォルダー内の PVS ライブラリの依存関係グラフを生成します。これらのスクリプトの詳細については、ここをクリックしてください。
(*) PVS 7.1 ディストリビューションにはすでに含まれています。
NASALib (v7.0.1) は、Visual Studio Code に基づく PVS への最新のグラフィカル インターフェイスである VSCode-PVS と完全な互換性があります。 NASALib の最新バージョンは VSCode-PVS からインストールできます。
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に追加します。存在しない場合は、このディレクトリのパスをコンテンツとしてのみ使用して、そのような変数を作成します。通常、シェル システムで起動時にこの変数を作成すると非常に便利です。この目的を達成するには、シェルに応じて、起動スクリプトに次のいずれかの行を追加するとよいでしょう。 C シェル (csh または tcsh) の場合、次の行を~/.cshrcに追加できます。
setenv PVS_LIBRARY_PATH " /nasalib " Borne シェル (bash または sh) の場合は、次の行を~/.bashrcまたは~/.profileに追加します。
export PVS_LIBRARY_PATH= " /nasalib " 以前に NASALib をインストールしていた場合は、ファイル~/.pvs.lispを削除するか、そのファイルに特別な構成がある場合は次の行を削除します
( load " /nasalib/pvs-patches.lisp " ) 最後に、ディレクトリ
install-scriptsコマンドは、必要に応じて NASALib スクリプトを更新およびインストールします。
$ ./install-scriptsNASALib の古いバージョンは、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 の形式手法チーム
セザール・ムニョス・マリアノ・モスカート
