パス

SPASSは、マックス・プランク計算機科学研究所で開発された、等号を含む一階述語論理の自動定理証明器であり、重ね合わせ計算を使用しています。元々は「Synergetic Prover Augmenting Superposition with Sorts」の略でした。この定理証明システムはFreeBSDライセンスの下で公開されています。^[¹^]

SPASS の拡張機能である SPASS-XDB は、外部ソースからの正の単位公理のオンザフライ取得のサポートを追加しました。^{[ 2 ]} SPASS-XDB は、リレーショナルデータベース、Web サービス、またはリンクされたデータサーバーからの事実を取り込むことができます。Mathematica を使用した算術のサポートも追加されました。^{[ 3 ]}

参考文献

↑ "Max-Planck-Institut für Informatik - ロジックの自動化: Spass"。Spas-prover.org。 2010-05-28 。2016 年 8 月 10 日に取得。
↑ Suda, Martin; Sutcliffe, Geoff; Wischnewski, Patrick; Lamotte-Schubert, Manuel; De Melo, Gerard (2009). "自動定理証明における公理の外部ソース" . KI 2009: 人工知能の進歩. Lecture Notes in Computer Science. Vol. 5803. pp. 281–288 . doi : 10.1007/978-3-642-04617-9_36 . ISBN 978-3-642-04616-22016年8月10日に取得。
↑ David Stanovsky; Martin Suda; Geoff Sutcliffe. "SPASS-XDB goes Mathematical" (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: 第 22 回自動推論に関する国際会議、Springer、pp . 140–145 。