proofsystems.tex

\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}


% ======================================================
% Proof Systems in Chronological Order

\includeProofSystem{PrincipiaMathematica} % 1910
\includeProofSystem{Frege} % 1893
\includeProofSystem{Hilbert} % 1917
\includeProofSystem{Bernays} % 1918
\includeProofSystem{HilbertAckermann} % 1928
\includeProofSystem{GentzenNJ} % 1935
\includeProofSystem{GentzenLK} % 1935
\includeProofSystem{GentzenLJ} % 1935
\includeProofSystem{EpsilonCalculus} % 1923, 1939
\includeProofSystem{KleeneG3classical} % 1952
\includeProofSystem{KleeneG3intuitionistic} % 1952
\includeProofSystem{MultiConclusionLJ} % 1954
\includeProofSystem{LambekCalc} % 1958
\includeProofSystem{Resolution} % 1965
\includeProofSystem{FolUnif} % 1965
\includeProofSystem{OrderedRes} % 1969
\includeProofSystem{Paramodulation} % 1969
\includeProofSystem{Completion} % 1970/1986
\includeProofSystem{fc} % 1971
\includeProofSystem{PreUnif} % 1975
\includeProofSystem{RK} % 1982
\includeProofSystem{ExpansionProofs} % 1983
\includeProofSystem{Bledsoe} % 1984
\includeProofSystem{Muscadet} % 1984
\includeProofSystem{ILL} % 1987
\includeProofSystem{LL} % 1987
\includeProofSystem{ProofNetMLL} % 1987
\includeProofSystem{StructSpec} % 1988
\includeProofSystem{PureTypeSystems} % 1989
\includeProofSystem{FILL} % 1990
\includeProofSystem{SignedLogics} %1990
\includeProofSystem{Superposition} % 1990/1994
\includeProofSystem{SaturationWithRed} % 1990
\includeProofSystem{LC} % 1991
\includeProofSystem{RefineSpec} % 1991
\includeProofSystem{LTLClausalResolution} % 1991/2001
\includeProofSystem{TLL} % 1992
\includeProofSystem{ConstraintSup} % 1992/1995
\includeProofSystem{HierarchicSup} % 1992/2013
\includeProofSystem{LambdaMu} % 1992
\includeProofSystem{LEI} % 1993
\includeProofSystem{LuoLF} % 1994
\includeProofSystem{LambdaBar} % 1994
\includeProofSystem{FIL} % 1995
\includeProofSystem{LuoLFC} % 1996
\includeProofSystem{G3c} % 1996
\includeProofSystem{CancellativeSup} % 1996
\includeProofSystem{GraphTabK} %1997
\includeProofSystem{SyntheticTableaux} % 2000
\includeProofSystem{LLP} %2000
\includeProofSystem{LKMuMuTilde} % 2000
\includeProofSystem{CSFour} % 2000
\includeProofSystem{HL} % 2001
\includeProofSystem{TC} % 2002/2014
\includeProofSystem{IHL} % 2003
\includeProofSystem{FOTLResolution} % 2003
\includeProofSystem{ModelEvolution} % 2003
\includeProofSystem{FOTLResolution} % 2003
\includeProofSystem{SocraticProofsCPL} % 2003
\includeProofSystem{SocraticProofsFOL} % 2004
\includeProofSystem{ModalSocraticProofsK} % 2004
\includeProofSystem{ModalSocraticProofs} % 2004
\includeProofSystem{LKMuMuTildeTree} % 2005
\includeProofSystem{LabelledConditionals} % 2003-2007
\includeProofSystem{KLM} % 2005-2009
\includeProofSystem{GBetaFB} % 2004-2009
\includeProofSystem{ExtResLEO2} % 2006-2013
\includeProofSystem{LKF} % 2007
\includeProofSystem{LJF} % 2007
\includeProofSystem{LambdaPiModulo} % 2007
\includeProofSystem{FOTLFineGrainedResolution} % 2009
\includeProofSystem{CTLClausalResolution} % 2009
\includeProofSystem{LambdaTermSequent} % 2011
\includeProofSystem{ParaconsistentSequentCalculi} % 2012
\includeProofSystem{Counterfactual} % 1983-2013
\includeProofSystem{Counterfactual2} % 2012-2013
\includeProofSystem{NestedConditionals} % 2012-2014
\includeProofSystem{FILL-dn} % 2013
\includeProofSystem{ContextualND} % 2013
\includeProofSystem{IR} % 2014
\includeProofSystem{SKMlin} % 2014
\includeProofSystem{EDResolutionCPL} % 2014
\includeProofSystem{EDResolutionmbC} % 2014
\includeProofSystem{MtSC} % 2014, 2016
\includeProofSystem{ModalNaturalDeduction} % 2015
\includeProofSystem{PolynomialRingCalculusWithOperators} % 2015
\includeProofSystem{ConflictResolution} % 2016
\includeProofSystem{negmodal} % 2016
\includeProofSystem{UpdateLogic} % 2016
\includeProofSystem{MtDInqL} % 2016
\includeProofSystem{MtDDEL} % 2016
\includeProofSystem{MtDLatL} % 2017
\includeProofSystem{MtDSDM} % 2017
\includeProofSystem{LJstar} % 2017
\includeProofSystem{QE-calculus} % 2017