Tractability of Cut-free Gentzen-type propositional calculus with permutation inference II

AbstractIn Arai (1996), we introduced a new inference rule called permutation to propositional calculus and showed that cut-free Gentzen system LK (GCNF) with permutation (1) satisfies the feasible subformula property, and (2) proves pigeonhole principle and k-equipartition polynomially. In this paper, we survey more properties of our system. First, we prove that cut-free LK+permutation has polynomial size proofs for nonunique endnode principle, Bondy's theorem. Second, we remark the fact that permutation inference has an advantage over renaming inference in automated theorem proving, since GCNF+renaming does not always satisfy the feasible subformula property. Finally, we discuss on the relative efficiency of our system vs. Frege systems and show that Frege polynomially simulates GCNF+renaming if and only if Frege polynomially simulates extended Frege