Proof search in multi-succedent sequent calculi for intuitionistic logics (Theory and Applications of Proof and Computation)

Abstract

In this note, terminating and bicomplete proof search procedures with respect to the Kripke semantics are given in multi-succedent sequent calculi for intuitionistic propositional logic and fragments of intuitionistic predicate logic. G. Mints [11, 12] in his later years investigated a proof search procedure in single-succedent sequent calculus for intuitionistic predicate logic.