シーケント計算の再解釈 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. 選言命題の希釈

導出 型環境の外移動