# Intellektik: Technical report 92-20

## Shortening Proofs by Quantifier Introduction

### U. Egly

In this paper, we describe an extended resolution calculus based on the
introduction of new existential quantifiers. The additional rule is called
Q-extension (quantifier extension). We show how polynomial
refutations can be obtained by applying Q-extension, whereas usual resolution
refutations are exponential. We compare our new deduction concept with
FR-deduction \cite{Baaz:Leitsch:1992} and generalized factorization
\cite{Egly:1991b}. Q-extension can simulate both concepts without
considerably increasing the length of a refutation. We present an example
where only Q-extension yields a refutation of linear length.