Session FOL_Seq_Calc2

Theories

• SeCaV
• FOL-Fitting.FOL_Fitting
• FOL_Seq_Calc1.Common
• FOL_Seq_Calc1.Tableau
• FOL_Seq_Calc1.Sequent
• Sequent1
• Sequent_Calculus_Verifier
• Collections.ICF_Tools
• Collections.Ord_Code_Preproc
• Collections.Locale_Code
• Abstract_Completeness.Abstract_Completeness
• Abstract_Soundness.Finite_Proof_Soundness
• Prover
• Export
• ProverLemmas
• Hintikka
• EPathHintikka
• Usemantics
• Countermodel
• Soundness
• Completeness
• Results