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

## TL;DR

This paper refines a bottom-up sequent calculus proof search procedure for minimal implicational logic, providing improved termination strategies, explicit bounds, and comprehensive soundness and completeness proofs.

## Contribution

It introduces a new termination strategy for the sequent calculus, with explicit bounds and an improved completeness proof for proof search in minimal implicational logic.

## Key findings

- Refined proof search termination strategy
- Explicit upper bounds on proof search
- Complete soundness and completeness proofs

## Abstract

In a previously published ENTCS paper (Santos et al. (2016)), we introduced a sequent calculus called $\mathbf{LMT^{\rightarrow}}$ for Minimal Implicational Propositional Logic ($\mathbf{LMT^{\rightarrow}}$). This calculus provides a proof search procedure for $\mathbf{LMT^{\rightarrow}}$ that works in a bottom-up approach. We proved there that $\mathbf{LMT^{\rightarrow}}$ 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{LMT^{\rightarrow}}$ 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.

---
Source: https://tomesphere.com/paper/1905.02059