コンパクト有向シーケント計算の規則

いくつかの事例、シーケント推論図の形式：

[Γ→Δ],[Π→Σ]⇒Γ,Π→Δ,Σ
 Γ→Δ  Π→Σ
 ===============(×)
 Γ,Π→Δ,Σ

[Γ→Δ,A], [A,Π→Σ]⇒[Γ,Π→Δ,Σ]
  (A has ↓)
  Γ→Δ,A  A,Π→Σ
 ====================(＼↓A)
    Γ,Π→Δ,Σ


[Γ→Δ,A],[Π→A*,Σ]⇒[Γ,Π→Δ,Σ]
  (A has ↓)
  Γ→Δ,A   Π→A*,Σ
 ======================(∪→A)
    Γ,Π→Δ,Σ

自然演繹証明図の変形として描くと：

[Γ→Δ],[Π→Σ]⇒Γ,Π→Δ,Σ
before
 Γ   Π
 ---  ---
  :    :
  :    :
 ---  ---
 Δ   Σ

after
 Γ,Π
 ------
   :
   :
 ------
 Δ,Σ


[Γ→Δ,A], [A,Π→Σ]⇒[Γ,Π→Δ,Σ]
before (A has ↓)
 Γ    A,Π
 ----  ----
  :     :
  :     :
 ----  ----
 Δ,A  Σ

after
  Γ,Π
  -----
    :
    :
  -----
  Δ,Σ


[Γ→Δ,A],[Π→A*,Σ]⇒[Γ,Π→Δ,Σ]
before (A has ↓)
  Γ    Π
  ---   ---
   :     :
   :     :
  ----  -----
  Δ,A  A*,Σ

after
  Γ,Π
  -----
    :
    :
  -----
  Δ,Σ

(＼↓A)の配置をソレらしくすると：

[Γ→Δ,A], [A,Π→Σ]⇒[Γ,Π→Δ,Σ]
before (A has ↓)
 Γ    :
 ---   :
  :    :
  :    :
 ----  :
 Δ,A  :
 :   A,Π
 :    ----
 :     :
 :     :
 :    ----
 :    Σ
after
  Γ,Π
  -----
    :
    :
  -----
  Δ,Σ