高解像度版はありません。
このファイルは、ウィキメディア・コモンズから呼び出されています。
このファイルは、他のプロジェクトで使用されている可能性があります。
このファイルの解説やノートへの記入、履歴などの詳細の確認は、ウィキメディア・コモンズのファイルページ (ノート /履歴 /ログ )を使用してください。
Can be replaced with following TeX equivalent when \bindnasrepma (⅋) is available:
A
⊢
A
i
n
i
t
Γ
1
⊢
A
,
Σ
1
Γ
2
,
A
⊢
Σ
2
Γ
1
,
Γ
2
⊢
Σ
1
,
Σ
2
c
u
t
Γ
⊢
Σ
Γ
,
!
A
⊢
Σ
w
e
a
k
L
Γ
⊢
Σ
Γ
⊢
?
A
,
Σ
w
e
a
k
R
Γ
,
!
A
,
!
A
⊢
Σ
Γ
,
!
A
⊢
Σ
c
o
n
t
r
L
Γ
⊢
?
A
,
?
A
,
Σ
Γ
⊢
?
A
,
Σ
c
o
n
t
r
R
Γ
,
A
,
B
⊢
Σ
Γ
,
A
⊗
B
⊢
Σ
⊗
L
Γ
1
⊢
A
,
Σ
1
Γ
2
⊢
B
,
Σ
2
Γ
1
,
Γ
2
⊢
A
⊗
B
,
Σ
1
,
Σ
2
⊗
R
Γ
⊢
Σ
Γ
,
1
⊢
Σ
1
L
⊢
1
1
R
Γ
,
A
⊢
Σ
Γ
,
A
&
B
⊢
Σ
&
L
1
Γ
,
B
⊢
Σ
Γ
,
A
&
B
⊢
Σ
&
L
2
Γ
⊢
A
,
Σ
Γ
⊢
B
,
Σ
Γ
⊢
A
&
B
,
Σ
&
R
n
o
⊤
L
Γ
⊢
⊤
,
Σ
⊤
R
Γ
1
,
A
⊢
Σ
1
Γ
2
,
B
⊢
Σ
2
Γ
1
,
Γ
2
,
A
∖
b
i
n
d
n
a
s
r
e
p
m
a
B
⊢
Σ
1
,
Σ
2
∖
b
i
n
d
n
a
s
r
e
p
m
a
L
Γ
⊢
A
,
B
,
Σ
Γ
⊢
A
∖
b
i
n
d
n
a
s
r
e
p
m
a
B
,
Σ
∖
b
i
n
d
n
a
s
r
e
p
m
a
R
⊥
⊢
⊥
L
Γ
⊢
Σ
Γ
⊢
⊥
,
Σ
⊥
R
Γ
,
A
⊢
Σ
Γ
,
B
⊢
Σ
Σ
,
A
⊕
B
⊢
Σ
⊕
L
Γ
⊢
A
,
Σ
Σ
⊢
A
⊕
B
,
Σ
⊕
R
1
Γ
⊢
B
,
Σ
Σ
⊢
A
⊕
B
,
Σ
⊕
R
2
Σ
,
0
⊢
Σ
0
L
n
o
0
R
Γ
,
A
⊢
Σ
Γ
,
!
A
⊢
Σ
!
L
!
Γ
⊢
A
,
?
Σ
!
Γ
⊢
!
A
,
?
Σ
!
R
!
Γ
,
A
⊢
?
Σ
!
Γ
,
?
A
⊢
?
Σ
?
L
Γ
⊢
A
,
Σ
Γ
⊢
?
A
,
Σ
?
R
C
L
L
s
e
q
u
e
n
t
c
a
l
c
u
l
u
s
{\displaystyle {\begin{array}{c}{\frac {}{A\vdash A}}\ \mathrm {init} \qquad {\frac {\Gamma _{1}\vdash A,\ \Sigma _{1}\quad \Gamma _{2},\ A\vdash \Sigma _{2}}{\Gamma _{1},\ \Gamma _{2}\vdash \Sigma _{1},\ \Sigma _{2}}}\ \mathrm {cut} \\\\{\frac {\Gamma \vdash \Sigma }{\Gamma ,\ !A\vdash \Sigma }}\ \mathrm {weak} _{L}\qquad {\frac {\Gamma \vdash \Sigma }{\Gamma \vdash ?A,\ \Sigma }}\ \mathrm {weak} _{R}\qquad {\frac {\Gamma ,\ !A,\ !A\vdash \Sigma }{\Gamma ,\ !A\vdash \Sigma }}\ \mathrm {contr} _{L}\qquad {\frac {\Gamma \vdash ?A,\ ?A,\ \Sigma }{\Gamma \vdash ?A,\ \Sigma }}\ \mathrm {contr} _{R}\\\\{\frac {\Gamma ,\ A,\ B\vdash \Sigma }{\Gamma ,\ A\otimes B\vdash \Sigma }}\otimes _{L}\qquad {\frac {\Gamma _{1}\vdash A,\ \Sigma _{1}\quad \Gamma _{2}\vdash B,\ \Sigma _{2}}{\Gamma _{1},\ \Gamma _{2}\vdash A\otimes B,\ \Sigma _{1},\ \Sigma _{2}}}\otimes _{R}\qquad {\frac {\Gamma \vdash \Sigma }{\Gamma ,\ 1\vdash \Sigma }}1_{L}\qquad {\frac {}{\vdash 1}}1_{R}\\{\frac {\Gamma ,\ A\vdash \Sigma }{\Gamma ,\ A\ \&\ B\vdash \Sigma }}\&_{L1}\quad {\frac {\Gamma ,\ B\vdash \Sigma }{\Gamma ,\ A\ \&\ B\vdash \Sigma }}\&_{L2}\quad {\frac {\Gamma \vdash A,\ \Sigma \quad \Gamma \vdash B,\ \Sigma }{\Gamma \vdash A\ \&\ B,\ \Sigma }}\&_{R}\quad {\begin{matrix}\\\mathrm {no} \ \top _{L}\end{matrix}}\qquad {\frac {}{\Gamma \vdash \top ,\ \Sigma }}\top _{R}\\\\{\frac {\Gamma _{1},\ A\vdash \Sigma _{1}\quad \Gamma _{2},\ B\vdash \Sigma _{2}}{\Gamma _{1},\ \Gamma _{2},\ A{\color {red}{\backslash bindnasrepma}}B\vdash \Sigma _{1},\ \Sigma _{2}}}{\color {red}{\backslash bindnasrepma}}_{L}\qquad {\frac {\Gamma \vdash A,\ B,\ \Sigma }{\Gamma \vdash A{\color {red}{\backslash bindnasrepma}}B,\ \Sigma }}{\color {red}{\backslash bindnasrepma}}_{R}\qquad {\frac {}{\bot \vdash }}\ \bot _{L}\qquad {\frac {\Gamma \vdash \Sigma }{\Gamma \vdash \bot ,\ \Sigma }}\ \bot _{R}\\\\{\frac {\Gamma ,\ A\vdash \Sigma \quad \Gamma ,\ B\vdash \Sigma }{\Sigma ,\ A\oplus B\vdash \Sigma }}\ \oplus _{L}\qquad {\frac {\Gamma \vdash A,\ \Sigma }{\Sigma \vdash A\oplus B,\ \Sigma }}\ \oplus _{R1}\qquad {\frac {\Gamma \vdash B,\ \Sigma }{\Sigma \vdash A\oplus B,\ \Sigma }}\ \oplus _{R2}\qquad {\frac {}{\Sigma ,\ 0\vdash \Sigma }}\ 0_{L}\qquad \mathrm {no} \ 0_{R}\\\\{\frac {\Gamma ,\ A\vdash \Sigma }{\Gamma ,\ !A\vdash \Sigma }}\ !_{L}\qquad {\frac {!\Gamma \vdash A,\ ?\Sigma }{!\Gamma \vdash !A,\ ?\Sigma }}\ !_{R}\qquad {\frac {!\Gamma ,\ A\vdash ?\Sigma }{!\Gamma ,\ ?A\vdash ?\Sigma }}\ ?_{L}\qquad {\frac {\Gamma \vdash A,\ \Sigma }{\Gamma \vdash ?A,\ \Sigma }}\ ?_{R}\\\\\mathrm {CLL\ sequent\ calculus} \end{array}}}
概要
元のアップロードログ
Date/Time
Dimensions
User
Comment
14:19, 5 January 2005
en:User:Quadell
(tagged)
02:12, 22 August 2004
620x390 (13361 bytes)
en:User:Kaustuv
(Gah! Uploaded wrong file by mistake. Please delete earlier versions.)
02:05, 22 August 2004
620x355 (11933 bytes)
en:User:Kaustuv
(correcting mistakes in the older version)
07:58, 2 June 2004
en:User:Kaustuv
(copyright info added)
07:51, 2 June 2004
en:User:Kaustuv
(barfs if something resembling a tag is in its description)
07:49, 2 June 2004
620x422 (15111 bytes)
en:User:Kaustuv
(rules as an image because <math> has no support for inference rules)
ファイルの履歴
過去の版のファイルを表示するには、その版の日時をクリックしてください。
日付と時刻 サムネイル 寸法 利用者 コメント
現在の版 2006年3月19日 (日) 15:37 620 × 390 (13キロバイト) Maksim La bildo estas kopiita de wikipedia:en. La originala priskribo estas: Inference rules for classical linear sequent calculus. {{GFDL}} For the linear logic page. This is intended as a stopgap measure until <math> matures more. Currently it does
ファイルの使用状況
グローバルなファイル使用状況