forked from ProofSystem/Encyclopedia
-
Notifications
You must be signed in to change notification settings - Fork 0
/
proofsystems.tex
72 lines (59 loc) · 2.99 KB
/
proofsystems.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
\part{\emph{Proof Systems}}
% When adding an entry for a proof system "X" to the encyclopedia,
% an "\includeProofSystem" statement with the following
% format should be added in this file :
% \includeProofSystem{X}
% ======================================================
% Acronyms of Proof Systems in Chronological Order
\newcommand{\NJ}{\ensuremath{\mathbf{NJ}}\xspace} % GentzenNJ 1935
\newcommand{\LK}{\ensuremath{\mathbf{LK}}\xspace} % GentzenLK 1935
\newcommand{\LJ}{\ensuremath{\mathbf{LJ}}\xspace} % GentzenLJ 1935
\newcommand{\LJmc}{\ensuremath{\mathbf{LJ'}}\xspace} % MultiConclusionLJ 1954
\newcommand{\SystemF}{\ensuremath{\mathbf{F}}\xspace} % fc 1971
\newcommand{\Bledsoe}{\ensuremath{\mathbf{Prover}}\xspace} % Bledsoe 1984
\newcommand{\Muscadet}{\ensuremath{\mathbf{Muscadet}}\xspace} % Muscadet 1984
\newcommand{\LF}{\ensuremath{\mathbf{LF}}\xspace} % LuoLF 1994
\renewcommand{\lambdabar}{\overline{\lambda}} % LambdaBar 1994
\newcommand{\LJT}{\ensuremath{\mathbf{LJT}}\xspace} % LambdaBar 1994
\newcommand{\Gtc}{\ensuremath{\mathbf{G3c}}\xspace} % G3c 1996
\newcommand{\LKmumutilde}{\ensuremath{\mathbf{LK}_{\mu\tilde\mu}}\xspace} % LKMuMuTilde 2000
\newcommand{\LKT}{\ensuremath{\mathbf{LKT}\xspace}} % LKMuMuTilde 2000
\newcommand{\LKQ}{\ensuremath{\mathbf{LKQ}\xspace}} % LKMuMuTilde 2000
\newcommand{\LKmumutildetree}{\ensuremath{\mathbf{LK}_{\mu\tilde\mu}-\mathbf{tree}}\xspace} % LKMuMuTildeTree 2005
\newcommand{\calcoloP}{{\bf $\mathcal{T}P^{\bf T}$}} % KLM 2005
\newcommand{\LKF}{\ensuremath{\mathbf{LKF}}\xspace} % LKF 2007
\newcommand{\LJF}{\ensuremath{\mathbf{LJF}}\xspace} % LJF 2007
\newcommand{\FILL}{\ensuremath{\mathbf{FILL}}\xspace} % FILL 1990
\newcommand{\NDc}{\ensuremath{\mathbf{ND}^\mathbf{c}}\xspace} % ContextualND 2013
\newcommand{\seqlcnxt}{\ensuremath{\mathbf{SKM_{lin}}}\xspace}) % SKMlin 2014
% ======================================================
% Proof Systems in Chronological Order
\includeProofSystem{GentzenNJ} % 1935
\includeProofSystem{GentzenLK} % 1935
\includeProofSystem{GentzenLJ} % 1935
\includeProofSystem{MultiConclusionLJ} % 1954
\includeProofSystem{fc} % 1971
\includeProofSystem{ExpansionProofs} % 1983
\includeProofSystem{Bledsoe} % 1984
\includeProofSystem{Muscadet} % 1984
\includeProofSystem{FILL} % 1990
\includeProofSystem{LambdaMu} % 1992
\includeProofSystem{LuoLF} % 1994
\includeProofSystem{LambdaBar} % 1994
\includeProofSystem{G3c} % 1996
\includeProofSystem{LKMuMuTilde} % 2000
\includeProofSystem{LKMuMuTildeTree} % 2005
\includeProofSystem{LabelledConditionals} % 2003-2007
\includeProofSystem{KLM} % 2005-2009
\includeProofSystem{GBetaFB} % 2004-2009
\mathversion{mathhungry}
\includeProofSystem{ExtResLEO2} % 2006-2013
\mathversion{normal}
\includeProofSystem{LKF} % 2007
\includeProofSystem{LJF} % 2007
\includeProofSystem{Counterfactual} % 1983-2013
\includeProofSystem{Counterfactual2} % 2012-2013
\includeProofSystem{NestedConditionals} % 2012-2014
\includeProofSystem{ContextualND} % 2013
\includeProofSystem{IR} % 2014
\includeProofSystem{SKMlin} % 2014