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
last changed by Hendrik
10 Apr 2013