1. 主な定理証明システムへのリンク
2. その他 (学会、プロジェクト、等へのリンク)

関連サイト1(定理証明システム)

1. Otter
   Otter は、アルゴンヌ国立研究所で開発された 一階述語論理の定理証明システムで、等式推論、項書換え処理、Knuth-Bendix 完備化 手続きの機能も持つ。 ベンチマークテスト上では安定したパフォーマンスを示しており、 定理証明研究において効率上の比較を行う際には、Otter との比較 により効率性を議論することが多い。 Otter の主な問題領域は、抽象代数や形式論理である。
   
   
2. FINDER
   FINDER (Finite Domain Enumerator) はオーストラリア国立大学の J.Slaney によって開発された有限モデル生成システムで、 全解探索によって入力節を満足するすべてのモデルを発見する。 入力節は一階述語論理の形式であるが、モデルの持つ有限次数を 指定するところが大きな特徴である。
   
   
3. 3TAP
   3TAP は、ドイツの Karlsruhe 大学で開発されたタブロー法に基づく 多値論理を対象とした定理証明システムである。
   
   
4. PTTP
   PTTP (Prolog Technology Theorem Prover) は元SRI の M.Stickel により 開発された Prolog の処理系を一階述語論理に拡張した定理証明システムで、 model elimination 法をベースとしている。 包摂テスト、デモジュレーション、重み付け優先などの戦略導入機能 等がないため、大規模な問題には不向きであるが、 推論実行上の効率の可能性を示すシステムである。
   
   
5. SETHEO
   SETHEO は当初、 ESPRIT プロジェクトの一貫として開発されたシステムであるが、その後、 ミュンヘン工科大学を中心として改良が行われてきたもので、 model elimination 法を一般化した コネクションタブロー法に基づく一階述語論理に関するトップダウン型の 定理証明システムである。

関連サイト2(その他)

1. CADE (Conference on Automated Deduction)
   定理証明研究における最もメジャーな学会のひとつ。
   
   
2. Automated Reasoning Project at Argonne
   アメリカのアルゴンヌ国立研究所における 定理証明プロジェクトのページ。
   
   
3. TPTP library (Mirror Site 1)
   TPTP library (Mirror Site 2)
   TPTP (Thousands of Problems for Theorem Provers) は、 自動定理証明システムのためのテストプログラム集で、定理証明システムの 効率比較のベンチマークとして広く使用されている。 主な定理証明システムに対するトランスレータも含まれている。 従来、定理証明システムの効率比較は、問題領域が分散していたり、表現方法が 異っていたりして、それぞれを比較することが困難であったが、TPTP は こうしたベンチマークテストを共通化することで、効率比較を同じプラットフォーム 上で行うことを目的としたものである。