search

meta-logic / sellf

SubExponential Linear Logic Framework for reasoning about sequent calculus systems
7 stars 2 forks source link

Better cut-elimination coverage #20

Open gisellemnr opened 6 years ago

gisellemnr commented 6 years ago

Use invertibility lemmas to have shorter proofs of cut-elimination