Loading article…
SNARK (SRI の New Automated Reasoning Kit) は、 SRI Internationalで開発された、人工知能およびソフトウェア エンジニアリングのアプリケーションを対象とした、マルチソートされた1 階論理の定理証明器です。
SNARK の主な推論メカニズムは、解決とパラモジュレーションです。さらに、アレンの時間間隔論理の制約ソルバーなど、特定のドメインに特化した決定手順も提供します。他の多くの定理証明器とは異なり、SNARK は完全に自動化されています (非対話型)。SNARK は、検索動作を調整するための多くの戦略的な制御を提供し、特定のアプリケーションに合わせてパフォーマンスを調整します。これに加えて、マルチソート ロジックの使用と、特殊目的の推論手順を汎用目的の推論と統合する機能により、SNARK は大規模なアサーション セットの推論器として特に適しています。
SNARK は、 NASAインテリジェント システム プロジェクトの推論コンポーネントとして使用されています。これはCommon Lispで記述されており、Mozilla パブリック ライセンスの下で利用可能です。
参照
参考文献
- M. Stickel、R. Waldinger、M. Lowry、T. Pressburger、および I. Underwood。「サブルーチン ライブラリからの天文学ソフトウェアの演繹的構成」第 12 回自動演繹に関する国際会議 (CADE-12) の議事録、フランス、ナンシー、1994 年 6 月、341 ～ 355 ページ。
- Richard Waldinger、Martin Reddy、Jennifer Dungan。「複数のデータ ソースの演繹的構成」。2002 年 5 月、インテリジェント データ理解研究タスク、インテリジェント システム プロジェクト、NASA SISM の進捗レポート。
- R、Waldinger、DE Appelt、J. Fry、DJ Israel、P. Jarvis、D. Martin、S. Riehemann、ME Stickel、M. Tyson、J. Hobbs、および JL Dungan。「複数のリソースからの演繹的質問応答」。New Directions in Question Answering、AAAI、2004 年。
- R. Waldinger、P. Jarvis、J. Dungan。「演繹法を使用して複数のデータ ソースを編成する」。Semantic Web Technologies for Searching and Retrieving、フロリダ州サニベル島、2003 年 10 月。
外部リンク
- SRIのSNARKホームページ
- SNARKチュートリアル