Loading article…
SPASSは、マックスプランク計算機科学研究所で開発され、重ね合わせ計算を使用した等式付き一階論理の自動定理証明器である。この名前は元々Synergetic Prover Augmenting Superposition with Sortsの略語であった。この定理証明システムはFreeBSDライセンスの下でリリースされている。[1]
SPASSの拡張機能であるSPASS-XDBは、外部ソースからの正単位公理のオンザフライ取得のサポートを追加しました。[2] SPASS-XDBは、リレーショナルデータベース、Webサービス、またはリンクデータサーバーからの事実を組み込むことができます。Mathematicaを使用した算術のサポートも追加されました。[3]
参考文献
- ^ "マックス・プランク情報研究所 - ロジックの自動化: Spass". Spas-prover.org。 2010-05-28 。2016 年 8 月 10 日に取得。
- ^ "Spass-Xdb". Cs.miami.edu . doi :10.1007/978-3-642-04617-9_36 . 2016年8月10日閲覧。
- ^ David Stanovsky、Martin Suda、Geoff Sutcliffe。「SPASS-XDB が数学的に進化」( PDF)。Karlin.mff.cuni.cz。2016年 8 月 10 日閲覧。
出典
- Weidenbach, Christoph; Dimova, Dilyana; Fietzke, Arnaud; Kumar, Rohit; Suda, Martin; Wischnewski, Patrick (2009)、「SPASS バージョン 3.5」、CADE-22: 22nd International Conference on Automated Deduction、Springer、pp. 140– 145。
外部リンク
- 公式サイト