発見・創発できる人工知能OTTER 論理パズルからのアプローチ

2020年4月26日

近代科学社

著者名：武藤佳恭、安藤類央

まえがき
目次

序章創発する自動推論エンジン
0.1 学習を超えた人工知能
0.2 天秤のコインのパズル
0.3 2インバータパズル
0.3.1 Graphvizを使った接続図の可視化
0.3.2 gprofを使った推論過程の検査
0.4 原始帰納関数

第1章 OTTERの基本
1.1 第三のプログラミングパラダイム－定理証明系
1.1.1 シンギュラリティとmimicking nature
1.1.2 オープンソース
1.1.3 正直者と嘘つき
1.1.4 プロトコル検証
1.2 三段論法
1.2.1 最初のプログラム
1.2.2 不完全性定理
1.2.3 ソクラテスの四段論法？
1.2.4 ソクラテスの四段論法？その2
1.3 モデル，世界，解釈
1.3.1 「三つの箱の中身を当てる」
1.3.2 モデルと解釈
1.3.3 節集合と矛盾
1.3.4 エルブラン領域
1.3.5 ロビンソンの分解原理と超導出
1.4 状態空間探索問題の表現方法
1.4.1 河渡り問題（状態空間探索）
1.4.2 河渡り問題その2「ヤギとオオカミとキャベツの河渡り」

第2章正直者と嘘つきの村のパズル― 一階述語論理
2.1 自動推論と整合性
2.2 パズルの概要
2.3 命題論理と一階述語論理
2.4 学習と創発
2.5 正直者と嘘つきの村
2.5.1 私たちはどちらかが嘘つき
2.5.2 私は嘘つきです
動作原理その1 プログラムの終わり方－空間と支持集号
動作原理その2 支持集号からの節の選択の仕方
2.5.3 AかBのどちらかが正直者です
2.5.4 論理積と論理和
2.5.5 私は嘘つきです（元に戻った村）
2.5.6 仮定の話をする人たちその1
2.5.7 数学的帰納法
2.5.8 仮定の話をする人たちその2
2.6 問題の核心
2.6.1 第2不完全性定理とその後
2.6.2 無限集合
2.6.3 ベキ集合
2.7 正直者と嘘つきのパズル発展版：吸血鬼の村

第3章自己増殖するロボットのパズル
3.1 OTTERとリスト処理
3.2 「使用」と「自己言及」－リシャールのパラドックス
3.3 基本的なリスト操作
3.4 惑星「オートマトン」のロボット
3.4.1 ロボットの名前
3.4.2 自分自身を生成するロボット
3.4.3 不動点定理と特殊記号文字列
3.4.4 特殊文字列と不動点原理
3.4.5 お互いを作り出すロボット
3.4.6 自分自身を破壊するロボット
3.4.7 恩知らずなロボット
動作原理その3 OTTERのメインループとdemodulation
3.5 ハノイの塔
3.6 停止問題と万能機械問題

第4章等価推論
4.1 paramodulationとdemodulation
4.2 代数系と自動推論
4.2.1 群の性質を証明する
4.2.2 環の性質を調べる
4.2.3 束の双対原理を証明する
4.3 15パズル
4.4 熱のヒューリスティクス
4.4.1 Moufang loop
4.4.2 Hot list strategy
動作原理その4 ヒューリスティクス（Hot List）の加え方

第5章 OTTERの過去・現在・未来
5.1 OTTER以前
5.2 OTTERの生い立ち
5.3 OTTERが人工知能の未来を占う？
5.4 ニューラルネットワークの歴史
5.4.1 1980年代：3種類のアルゴリズムが出揃う
5.4.2 1990年代：非線形問題
5.4.3 2000年代以降：データマイニング
5.5 プログラム言語の歴史
5.5.1 1970年代：CとProlog
5.5.2 1980年代：PCの普及と開発環境の発達
5.5.3 1990年代：オブジェクト指向の時代
5.5.4 2000年代：スケーラビリティ
5.6 定理証明系の歴史
5.6.1 1980～1990年代：高階論理や対話的処理の導入
5.6.2 2000年代：実装の多様化
5.6.3 2000年代以降：最近の定理証明系の成果
5.7 OTTERの未来
5.7.1 OTTERの参考実装としての有効性
5.7.2 ドメイン特化言語とOTTER
5.7.3 シンギュラリティとOTTER