Previous: TR 92-19 Next: TR 92-21

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.

Full Paper: Compressed postscript Compressed DVI

BibTeX entry