証明ストリング図
ストリング図とストリンググラフの関係を使い、グラフ理論的な操作として証明行為＝リーズニングを理解する。
キーワード（大事な言葉）の定義：
- 推論ノード：通常の推論規則を表す。複数（0個もあり）の入力（仮定）と1つの出力（結論）を持つ。
- ワイヤー：命題（論理式）でラベルされている。
- 補助ノード： コピーノード、破棄ノード、ラムダノード、交差（crossing）ノードなど。
- 進入境界：ストリンググラフの概念
- 退出境界：ストリンググラフの概念
- マージ：併置と同じ。直和グラフを作ること
- カット結合：シーケントのカット規則に相当
- ブランチ：ひとつのノード（推論ノード、補助ノード）と隣接する命題頂点からなる部分グラフ、スパイダーと同じ。
- 許容ブランチセット（admissible branch set）：「正しい」と認めるブランチの集まり
- 正しい証明ストリング図：すべてのブランチが許容ブランチセットに入っている。
証明ストリング図の特徴と注意
- 正しい証明ストリング図であっても、ツリーとは限らない。コピーブランチと∧-導入ブランチの縦結合はダイヤモンド形を含む。
- 正しい証明ストリング図であっても、DAGとは限らない。ラムダノードはサイクルを作る。
証明ストリング図は、描き変え規則で描き変えられる。
否定を矛盾で定義している場合などは、ラベルである論理式自体が置き換えられる。これはラベルの書き換え。描き変えではない。描き変えには部分グラフとしてのリデックスがあり、描き変え結果としてのリザルタント（コントラクタム）がある。
描き変え リデックス→リザルタント では、境界保存条件が課せられる。通常のタクティクでは、ゴール＝未知ノードからサブゴールズを生成するのを問題にするので、境界保存条件が全く見えなくなる。
