Abstract

Both at the propositional and the predicate level, in tableau systems of intuitionistic logic as well as in the corresponding sequent and natural calculi, the problem arises of reducing as much as possible the duplication of formulas, i.e., the reuse of formulas already used in a proof, in order to single out efficient proof search techniques. This problem has been analyzed in a paper by Dyckhoff, where a nearly optimal solution is given for intuitionistic propositional sequent and natural calculi, and in previous papers by the authors, where an improvement is proposed of Fitting's tableau system for intuitionistic predicate logic. In the present paper we reanalyze the ideas of our previous works in the light of Dyckhoff's results. This gives rise to a tableau system for intuitionistic predicate logic which provides a good improvement of the previous tableau systems with respect to the problem of duplication. The formal setting of the paper seems to be promising to treat further intermediate logics. In this line, we analyze Kuroda logic and provide for it a tableau system involving a smaller amount of duplication than the one involved in the intuitionistic tableau system presented in the paper