A Sequent Calculus Proof Search Procedure and Counter-model Generation based on Natural Deduction Bounds

Jefferson de Barros Santos, Bruno Lopes Vieira, Edward Hermann Haeusler

In a previously published ENTCS paper (Santos et al. (2016)), we introduced a sequent calculus called $\mathbf{LM}{\mathbf{T}}^{\to }$ for Minimal Implicational Propositional Logic ($\…