---
title: "On the Polynomial Transparency of Resolution"
authors:
  - "Reinhold Letz"
doi: ""
url: "https://ijcai.org/proceedings/1993/18"
pdf: "https://ijcai.org/proceedings/1993/0018.pdf"
venue: "Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence"
year: 1993
pages: "123-130"
track: "Automated Reasoning"
keywords:
---

# On the Polynomial Transparency of Resolution

Reinhold Letz

*Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence*, pages 123-130.

## Abstract

In this paper a framework is developed for measuring the complexities of deductions in an abstract and computationally perspicuous manner. As a notion of central importance appears the so-called polynomial transparency of a calculus. If a logic calculus possesses this property, then the complexity of any deduction can be correctly measured in terms of its inference steps. The resolution calculus lacks this property. It is proven that the number of inference steps of a resolution proof does not give a representative measure of the actual complexity of the proof, even if only shortest proofs are considered. We use a class of formulae which have proofs with a polynomial number of inference steps, but for which the size of any proof is exponential. The polynomial intransparency of resolution is due to the renaming of derived clauses, which is a fundamental deduction mechanism. This result motivates the development of new data structures for the representation of logical formulae.