シーケント計算の再解釈 4

メタリーズニングの種類：

1. ApplyReasoning : reas, deriv ≡> deriv
2. ComposeReasoning : reas, reas ≡> reas
3. ProductReasoning : reas, reas ≡> reas

リーズニング 導出のマージ：

1. MergeConj : conj → conj, con → conj ⇒ conj → conj
2. MergeDisj : conj → disj, con → disj ⇒ conj → disj
3. MergeConjLDist : conj → prop, con → disj ⇒ conj → disj
4. MergeConjRDist : conj → disj, con → prop ⇒ conj → disj
5. MergeDisjLDist : conj → prop, con → conj ⇒ conj → conj
6. MergeDisjRDist : conj → conj, con → prop ⇒ conj → conj

リーズニング 導出の結合：

1. Comp : conj → xxx, xxx → xxx ⇒ conj → xxx カット
2. PostComp : conj → xxx ⇒ conj → xxx 知識ベース使用
3. PreComp : conj → xxx ⇒ conj → xxx 知識ベース使用

リーズニング 導出のカリー化：

1. 右カリー化
2. 左カリー化

導出 族の濃縮

1. 連言族の濃縮
2. 選言族の濃縮

導出 命題の希釈

1. 連言命題の希釈
2. 選言命題の希釈

導出 型環境の外移動

まとめ

1. リーズニング 導出のマージ モノイド積
2. リーズニング 導出の結合 結合
3. リーズニング 導出のカリー化 指数
4. 導出 型環境の外移動
5. 導出 族の濃縮
6. 導出 命題の希釈