Resolution is cut-free (Q972424)

The paper proves through syntactic translation that the extension of the resolution proof system to deduction modulo is equivalent to the cut-free fragment of the sequent calculus modulo. The resolution method in deduction modulo, called ENAR, is proved to be sound with respect to the cut-free fragment of sequent calculus. However, in order to prove completeness of ENAR with respect to the original sequent calculus, extra assumptions are needed. Due to the expressiveness of deduction modulo, the results obtained in this paper can be applied to higher-order resolution, Peano arithmetic and Zermelo set theory.