4 problems

Consider extending the cut-elimination proof for the multiplicative-additive Lambek calculus with subexponential and bracket modalities, which uses “deep cut elimination” for $!$-f…

Let $\mathsf{LNS^{\infty}_{LTL}}$ be the non-wellfounded linear nested sequent calculus for linear temporal logic. Syntactic cut-elimination conjecture. The additional structural e…

A proof forest consists of the cut-reduction system described in the paper, with reductions generated by its cut-reduction rules. Strong normalization conjecture. The cut-reduction…

Strong normalization conjecture. The cut-reduction rules are strongly normalizing: every reduction sequence is of finite length.