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

Abstract

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 ($\mathbf{LM}{\mathbf{T}}^{\to }$). This calculus provides a proof search procedure for $\mathbf{LM}{\mathbf{T}}^{\to }$ that works in a bottom-up approach. We proved there that $\mathbf{LM}{\mathbf{T}}^{\to }$ is sound and complete. We also suggested a strategy to guarantee termination of the proof search procedure. In this current paper, we refined this strategy and presented a new strategy for $\mathbf{LM}{\mathbf{T}}^{\to }$ termination. Considering this new strategy, we also provide a (new) completeness proof for the system, which improves the previous version. Besides that, we present explicit upper bounds on the proof search procedure, derived from this new strategy. We also provide a full soundness proof of the system.