Abstract

We propose an extended resolution calculus called δm-resolution, aiming at reducing the length of the proofs without increasing too much the branching factor of the procedure. The soundness and refutational completeness of the new calculus is proven. We provide numerous examples showing the possibilities of our calculus and we show that δm-resolution allows to reduce the length of proof by a double exponential factor. We compare our calculus with the quantifier introduction method developed by Baaz, Leitsch and Egly and prove that both techniques are theoretically incomparable in the sense that none of them can polynomially simulate the other