Propositional_Proof_Systems

Formulas

Sema

Substitution

Substitution_Sema

CNF

CNF_Formulas

CNF_Sema

CNF_Formulas_Sema

CNF_To_Formula

Tseytin

Tseytin_Sema

MiniFormulas

MiniFormulas_Sema

Consistency

Compactness

Compactness_Consistency

Sema_Craig

SC

SC_Cut

SC_Depth

SC_Gentzen

SC_Sema

SC_Depth_Limit

SC_Compl_Consistency

ND

ND_Sound

ND_Compl_Truthtable

ND_Compl_Truthtable_Compact

HC

HC_Compl_Consistency

Resolution

Resolution_Sound

Resolution_Compl

Resolution_Compl_Consistency

HCSC

SCND

NDHC

HCSCND

LSC

LSC_Resolution

ND_FiniteAssms

ND_Compl_SC

Resolution_Compl_SC_Small

Resolution_Compl_SC_Full

MiniSC

MiniSC_HC

MiniSC_Craig