Theorem Proving and Partial Proof Search for Intuitionistic Propositional Logic Using a Permutation-free Calculus with Loop-Checking
Jacob M. Howe · Kent Academic Repository (University of Kent) · 1996
Backwards proof search and theorem proving with the standard cut-free sequent calculus for the propositional fragment of intuitionistic logic, Gentzen’s LJ , is inefficient for three reasons. Firstly the proof search is not in general terminating, due to the possibility of looping. Secondly it will produce proofs which are essentially the same; they are permutations of each other, and correspond to the same natural deduction. Thirdly there are choice points where it has to be decided which of several rules to apply. The sequent calculus MJ for intuitionistic logic was introduced (with another name, LJT ) by Herbelin in [Herb95]. This uses Girard’s idea of a special place for formulae in the antecedent, the stoup first seen in [Gir91]. The calculus was developed by Dyckhoff and Pinto [DP96a, DP96b] because it has the property that proofs are in 1-1 correspondence with the normal natural deductions. MJ is a permutation-free sequent calculus; it avoids the problems of permutations that the cut-free sequent calculus of Gentzen has. The propositional fragment of the calculus MJ is displayed in Figure 1. This removes the second of the problems (and partly addresses the third). However, the naive implementation of this calculus will lead to the possibility of looping.