Loading article…
自動推論ハンドブック（ISBN 0444508139、2128ページ）は、 自動推論の 分野に関する調査記事のコレクションです。2001年6月にMIT Pressから出版され、 John Alan RobinsonとAndrei Voronkovが編集しています。第1巻では、古典論理、等式およびその他の理論を含む第1階述語論理、および帰納法の方法について説明しています。第2巻では、高階論理、非古典論理、およびその他の種類の論理 について説明しています。
索引
第1巻
- 歴史
- マーティン・デイビス「自動演繹の初期の歴史」3～15ページ。
- 古典論理
- Leo Bachmair、Harald Ganzinger . Resolution Theorem Proving、pp. 19–99。
- ライナー・ヘンレ。タブローと関連手法、pp.100–178。
- アナトリ・デグチャレフ、アンドレイ・ヴォロンコフ。逆法、179 ～ 272 ページ。
- Matthias Baaz、Uwe Egly、Alexander Leitsch。正規形変換、pp. 273–333。
- アンドレアス・ノネンガルト、クリストフ・ヴァイデンバック。小節正規形の計算、335 ～ 367 ページ。
- 平等とその他の理論
- Robert Nieuwenhuis、Alberto Rubio。パラモジュレーションベースの定理証明、pp. 371–443。
- フランツ・バーダー、ウェイン・スナイダー『統一理論』445-532頁。
- Nachum Dershowitz、David Plaisted。Rewriting、pp.535-610。
- アナトリ・デグチャレフ、アンドレイ・ヴォロンコフ。シーケンスベースの計算における等価推論、611 ～ 706 ページ。
- Shang-Ching Chou、Xiao-Shang Gao。幾何学における自動推論、pp. 707–749。
- Alexander Bockmayr、Volker Weispfenning。数値制約の解決、pp. 751–842。
- 誘導
- アラン・バンディ『数学的帰納法による証明の自動化』845～911ページ。
- ヒューバート・コモン。帰納法なしの帰納法、pp.913-962。
第2巻
- 高階論理と論理フレームワーク
- ピーター・B・アンドリュース. 古典型理論、pp.965-1007。
- Gilles Dowek. 高階統一とマッチング、pp. 1009–1062。
- フランク・フェニング.論理フレームワーク、pp.1063-1147。
- ヘンク・バレンドレット、ヘルマン・グーヴァース。依存型システムを使用した証明アシスタント、1149 ～ 1238 ページ。
- 非古典的論理
- Jürgen Dix、Ulrich Furbach、Ilkka Niemelä。非単調推論：効率的な計算と実装に向けて、pp. 1241–1354。
- Matthias Baaz、Christian Fermüller、Gernot Salzer。多値論理の自動演繹、pp. 1355–1402。
- ハンス＝ユルゲン・オールバッハ、アンドレアス・ノネンガルト、マールテン・デ・ライケ、ドヴ・ガベイ。古典論理における 2 値の非古典論理のエンコード、1403 ～ 1486 ページ。
- アリルド・ヴァーラー。非古典的論理における接続、pp. 1487–1578。
- 決定可能なクラスとモデル構築
- ディエゴ・カルバネーゼ、ジュゼッペ・デ・ジャコモ、マウリツィオ・レンツェリーニ、ダニエレ・ナルディ。 『表現的記述ロジックにおける推論』、1581 ～ 1634 ページ。
- エドモンド・クラーク、ホルガー・シュリングロフ。モデル チェック、1635 ～ 1790 ページ。
- クリスチャン・フェルミュラー、アレクサンダー・ライチュ、ウルリッヒ・フシュタット、タネル・タメット。決議決定手順、1791 ～ 1849 ページ。
- 実装
- IV ラマクリシュナン、R.セカール、アンドレイ ヴォロンコフ。用語索引付け、1853 ～ 1964 ページ。
- Christoph Weidenbach. 重ね合わせ、ソート、分割の組み合わせ、pp. 1965–2013。
- Reinhold Letz、Gernot Stenz。モデル除去と接続 Tableau 手順、pp. 2015–2114。
外部リンク
- MIT プレスページ