タクティクのためのゲンツェン法則

Lean 論理
  1. Ident 公理
  2. Cut オペラッド結合
  3. Weak 水増し
  4. Cont 冗長性縮約 contraは矛盾
  5. Perm 交換
  6. CtxAndIntroL
  7. CtxAndIntroR
  8. CtxtOrIntro
  9. CtXImpIntro （LJ変形）
  10. CtxNotIntro
  11. CtxUnivIntro
  12. CtxExIntro
  13. TrgAndIntro
  14. TrgOrIntroL
  15. TrgOrIntroR
  16. TrgImpIntro
  17. TrgNotIntro
  18. TrgUnivIntro
  19. TrgExIntro

バックワード規則

  1. BKW Ident ≒ assumption
  2. BKW CtxSharpen
  3. BKW TrgAndIntro ＝ TrgAndSplit
  4. BKW TrgOrIntroL ＝ TrgOrElimL
  5. BKW TrgOrIntroR ＝ TrgOrElimR
  6. BKW TrgImpIntro ＝ TrgImpElim
  7. BKW TrgNotIntro ＝ TrgByContra
  8. BKW TrgUnivIntro ＝ TrgUnivElim
  9. BKW TrgExIntro ＝ TrgExElim

リライトは等式的な変形なので別な話。