Browse the Cut Elimination Formalization

Library enhancements: Material missing from Coq's standard library

misc sets lists list_set assoc some_nth classic image

Special Purpose Libraries: special purpose data types

functions dep_lists reorder list_multiset list_support some_neg dsets cast

Category theory:

functor slice

Logic basis:

formulas rules rule_sets admissibility substitution renaming modal_formulas plain_prop_mod

Logic Library:

sequent_support build_proof backward_substitution factor_subst factor_two_subst some_neg_form

Generic results from Section 3:

weakening inversion cut_properties

Propositional fragment: Required Results about Propositional Logic

propositional_formulas propositional_rules propositional_properties propositional_models propositional_sound build_prop_proof propositional_completeness

Semantics:

semantics one_step_conditions step_semantics

Soundness / Completeness (Section 4):

prop_mod sound complete

Syntactic cut elimination (Section 5):

generic_cut absorb contraction osr_cut mixed_cut prop_cut syntactic_cut

K Example:

k_syntax k_semantics k_sound_complete k_absorb k_nd

Other:

ck

Import all:

all

Coqdoc generated pages:

Coqdoc TOC Index