Session Propositional_Proof_Systems
View
theory dependencies
View
document
View
outline
Theories
HOL-Library.Old_Datatype
File ‹~~/src/HOL/Tools/Old_Datatype/old_datatype.ML›
HOL-Library.Nat_Bijection
HOL-Library.Countable
File ‹~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML›
Formulas
Sema
Substitution
Substitution_Sema
HOL-Library.Case_Converter
File ‹case_converter.ML›
HOL-Library.Simps_Case_Conv
File ‹simps_case_conv.ML›
CNF
CNF_Formulas
CNF_Sema
CNF_Formulas_Sema
HOL-Library.List_Lexorder
CNF_To_Formula
Tseytin
Tseytin_Sema
MiniFormulas
MiniFormulas_Sema
Consistency
Compactness
Compactness_Consistency
Sema_Craig
HOL-Library.Cancellation
File ‹Cancellation/cancel.ML›
File ‹Cancellation/cancel_data.ML›
File ‹Cancellation/cancel_simprocs.ML›
HOL-Library.Multiset
File ‹multiset_simprocs.ML›
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
HOL-Library.While_Combinator
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