Proof-search in natural deduction calculi for IPL

ABSTRACT. We address the problem of proof-search in the natural deduction calculus Ni for intuitionistic propositional logic (IPL). Our aim is to improve the usual n\"aive proof-search procedure where introduction rules are applied upwards and elimination rules downwards. In particular, we introduce Nbu, a sequent-style variant of Ni and we show that its derivations can be reduced in $\theta$-NF, a normal form (stronger than the usual one) where applications of $\lor E$ and $\to I$ satisfy additional conditions involving an evaluation relation $\theta$. This limits the application of such rules in proof-search and restricts the search space.