Session Propositional_Proof_Systems

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