Proof-search in natural deduction calculus for classical propositional logic

Abstract

We address the problem of proof-search in the natural deduction calculus for Classical propositional logic. Our aim is to improve the usual na¨ıve proof-search procedure where introduction rules are applied upwards and elimination rules downwards. In particular, we introduce Ncr, a variant of the usual natural deduction calculus for Classical propositional logic, and we show that it can be used as a base for a proof-search procedure which does not require backtracking nor loop-checking.