Implementing proof systems for the intuitionistic propositional logic

Abstract

Logical reasoning is something human beings consistently utilise to make decisions. The simplest calculus for proof search is the Natural Deduction. However, it is harder for an automated system to automate proof search using this calculus. At every step it has to decide the next step on the basis of: • which inference rule to apply at every decomposition level? • what sub goals should we prove in our pursuit to prove the final goal? • if the proof search is in a stuck state should we backtrack the proof search or terminate it? Analysis shows that if the proof search is carried out using the Sequent Calculus the number of choices required at each step are reduced. Hence our approach to minimise the high level of non determinism in Natural Deduction is to compute the proof search in the Sequent Calculus then translate it to the Natural Deduction. The advantage of this approach is that although the final proof search is expressed in the Natural Deduction Calculus the actual proof search is computed in the Sequent Calculus which reduces non determinism during proof computation. Furthermore, for the points highlighted above proof search in the Sequent Calculus eliminates the possibility of backtracking and restricts the number of inference rules applicable for certain propositions. Another advantage of this approach is that since the proof search is carried out in the Sequent Calculus, if the proof search in the Sequent Calculus is correct, by the correspondence between the Sequent Calculus and the Natural Deduction we are guaranteed that the same proof translated to Natural Deduction is also correct.