On the Polynomial Transparency of Resolution

1 Introduction

The competitiveness of logic calculi is essentially deter­ mined by two complementary factors; on the one hand, by the ability to provide compact proofs, and on the other, by the effort needed for finding such proofs, that is, by the search spaces induced by the indeterminism inherent in the calculi. In this paper, we shall system­ atically address the problem how to measure the first of these two capabilities of a calculus-its indeterministic power-in an abstract and nevertheless computationally reliable manner.

The paper consists of two parts, a conceptual part and an application part. In the conceptual part, we present a general framework for measuring the computational complexities of arbitrary transition relations and deduc­ tions, which are treated as particular transition relations. In order to be able to compare complexities on a level which is as abstract as possible, we subscribe to abstrac­ tions modulo polynomials, as usual in complexity theory. The central notions emerging this way are the properties of polynomial transparency and weak polynomial trans­ parency. The polynomial transparency of a transition relation guarantees that the number of rewrite steps in any transition sequence represents an adequate measure for the actual computational complexity of the sequence. Weak polynomial transparency is the adequate concept for evaluating the indeterministic powers of special tran­ sition relations, called proof relations, by restricting at­ tention to shortest proofs only.

·This work was financially supported by the Esprit Basic Research Actions 3125 Medlar I and 6471 Medlar II.

The benefit of the framework is twofold, not only does it facilitate the classification of deduction systems, it also may give advice how to improve the systems. This is il­ lustrated in the application part of this paper where the developed notions are used on the resolution calculus. It is proven that resolution lacks polynomial transparency, both in the strong and in the weak sense. As a conse­ quence, the number of inference steps of a shortest res­ olution proof does not give a representative measure of the actual complexity of the proof. The use of number terms in the object language can remedy this weakness for a certain class of formulae. Whether a general rem­ edy exists remains an open problem.

2 Complexity Measures for Deductions

The indeterministic power of a calculus is determined by the complexities of shortest proofs. This raises the fundamental question how the complexities of proofs and deductions in general should be measured.

2.1 Deduction Processes as Transition Relations

For investigations into the computational complexity of logic calculi, it is important to realize that deductions can be given a declarative and a process interpretation. According to the declarative reading, deductions are typ­ ically defined as sequences of formulae D = Fa, ... , Fn where each Fi, 1 ::::; i ::::; n, is derivable by applying an inference rule to formulae in D with an index stricly less than i. Another popular interpretation is to define de­ ductions as trees of formulae where each parent node can be derived from its immediate successors. There is no limitation to further ways of defining deductions. Deductions as static objects of the type mentioned above tend to be non-operational, in the sense that they do not prescribe the precise methodology according to which they have to be constructed. A deduction process can be viewed as one particular way of building up a de­ duction object. From a complexity point of view, the deduction process is the more fundamental notion and the deduction object is just a-even though extremely useful-by-product of the deduction process. 1

The most natural and general specification approach for the description of deduction processes is to model them as binary transition relations between structures of logical expressions, which play the role of the states in the transition relations. Typically, these states are finite sets of formulae, in general, they may be arbitrary finitistic set-theoretic objects, or strings encoding such objects. The binary transition relation 1- of the deduc­ tion processes defined by a calculus is determined by the inference rules of the calculus. 2 Like for the logical con­ sequence relation, the notions of deductions-we will call them derivations--and proofs can be introduced for the state transition relation 1-. A derivation in a transition relation 1- is a sequence D of states such that for each pair of successive states Si and Si+l in D: Si 1- Si+l· Proofs can be defined by associating with a given tran­ sition relation 1- a collection of input states :E, and a distinguished staten, named the success state. We shall call such transition relations proof relations. Then, any finite derivation in 1- with an initial state S E :E and terminal state n is said to be a proof of S in 1-. Using some notation from the field of reduction relations, given a transition relation 1-, we abbreviate with 1-k the k-fold composition of 1-. The (minimal) distance between any pair (S, S') of states in the transitive closure of a tran­ sition relation 1- is defined as min( {k I S 1-k S'} ), and abbreviated with 8(S, S', 1-) .

2.2 Three Natural Measures for Derivations

For evaluating the complexity of a derivation So, .. . , Sn in a transition relation 1-, three different measures are the obvious alternatives, which correspond to three dif­ ferent degrees of precision. The finest measure charges the minimal computing cost needed in a basic machine model to come from the initial state So to the terminal state Sn via the given intermediate states in the deriva­ tion. The computing cost of rewriting a state Si to a state Si+l may be, for example, the minimal number of configurations of a nondeterministic Turing machine (or the machine operations of the indeterministic version of any alternative realistic machine model? to transform si into Si+1 . Conceptually, the chosen basic machine model can be viewed as another (more elementary) transition relation, written - . Then, the elementary computing cost of the derivation D =So, ... , Sn can be defined as

1 This evaluation can be justified by recalling under which conditions a given object is accepted as a deduction of a type S, namely, if there exists a procedure which decides whether the object has type S . And the true complexity of a deduc­ tion object is the complexity of this verification procedure (for further motivation, consult [Letz, 1993]).

2 As a matter of fact, 1- does not denote the standard log­ ical consequence relation.

3 A realistic machine model can be defined to be any ma­ chine model in which the elementary operations are poly­ nomially related to the configurations of Turing machines

Taking the elementary computing cost of a derivation as the measure of its complexity has certain disadvan­ tages. First, for the standard realistic machine models, the measure is too detailed to be interesting as a quantity of comparison on a higher level of abstraction. Second, its value may vary strongly, depending on the chosen re­ alistic machine model-even though only up to polyn~ mials. Lastly, it may be very difficult to actually obtain the realistic computing cost, because the mapping down of high-level transition steps into basic machine opera­ tions is normally not carried out explicitly, instead one is satisfied with knowing about the possibility of such a transformation and its computational invariances.

An advance is offered by disregarding the elementary computing cost and restricting oneself to a higher level of representation, by only considering the size of a deriva­ tion D = So, ... , Sn, which is simply the sum of the (string) sizes of the states in D:

The highest abstraction level even ignores the size of a derivation D =So, ... , Sn and considers only the number of rewrite steps in the top-level transition relation 1-, in terms of logic calculi, the number of inference steps:

Eventually, it is this measure that is being striven for. It has been used successfully for analyzing the indeter­ ministic powers of many propositional calculi, for exam­ ple, in [Reckhow, 1976], [Haken, 1985], and various other papers. The abstraction performed by these authors is an abstraction modulo polynomials; they make plausi­ ble that the elementary computing cost is polynomially bounded by the number of inferences. Such an abstrac­ tion is very natural in that it takes into account the problem area of NP vs coNP, on the one hand, and ad­ ditionally leaves aside uninteresting subpolynomial dif­ ferences which result from the choice of the realistic ma­ chine model, on the other.

2.3 Polynomial Size- and Step-Transparency

The following two notions are fundamental for a general theory of the abstraction modulo polynomials. First, we consider the abstraction step from the elementary computing cost to the size of a derivation, and state under which condition such an abstraction is permissible.

Definition 1 [Polynomial size-transparency] A transi­ tion relation 1- is called polynomially size-transparent if there is a polynomial p such that for every derivation D = So, . .. , Sn in 1-:

(cf. the further remarks in [van Emde Boas, 1990] and [Letz, 1993]).

If a transition relation 1- is polynomially size­ transparent, then the size of any derivation gives a rep­ resentative complexity measure of its elementary com­ puting cost, as long as we are interested in complexities modulo polynomials. Polynomial size-transparency gen­ eralizes a basic concept introduced by Cook and Reck­ how in [Cook and Reckhow, 1974]. They define a (com­ plete) proof system as a (surjective) in polynomial time computable function from the set of strings to the set of valid formulae . Apparently, any proof system is polyno­ mially size-transparent.

In order to define a general criterion which guarantees that we can even abstract from the size of a derivation, it is necessary to use polynomials in two arguments.

Definition 2 [Polynomial (step-)transparency] A tran­ sition relation 1- is called polynomially step-transparent or just polynomially transparent if there is a polyno­ mial p in two arguments such that for every derivation D = So , ... , Sn in 1-:

If a transition relation is polynomially transparent, then the input size and the number of rewrite steps of any derivation give a representative measure of the com­ plexity of the derivation.

Note It is apparent that indeed a polynomial in two arguments is needed, demanding that cost(D) < p(n) does not result in a useful notion. As an example, con­ sider a calculus which solely can check whether a log­ ical formula has the structure F V -.F. According to the intended reading of inference steps, we wish to say that the calculus can verify its input in a single infer­ ence step. However, there is no complexity function (and hence no polynomial) which bounds the elementary com­ puting cost for verifying formulae of arbitrary size that have the shape F V -.F.

Clearly, if a transition relation 1- is polynomially trans­ parent, then 1- is polynomially size-transparent.

2.4 A Sufficient Condition for Polynomial Transparency

It is apparent that polynomial transparency is a highly desirable property. 4 The question is now how to deter­ mine whether a transition relation is polynomially trans­ parent. Polynomial transparency is a property defined on derivations of arbitrary lengths. It would be very comfortable if the polynomial transparency of a tran­ sition relation could be derived from more elementary properties of the transition relation. A very useful suffi­ cient condition for polynomial transparency, which only takes into account the step behaviour of a transition re­ lation, can be defined as follows.

4 Also, the concept of polynomial transparency leads to a natural generalization of the notion of a realistic machine model. By a generalized realidic machine model we can un­ derstand any computation model which, as a transition re­ lation, is polynomially transparent and has the expressive power of Turing machines.

Definition 3 [Polynomial time step-reliability] A transi­ tion relation 1- is called polynomial time step-reliable if there is a polynomial p such that for any one-step deriva­ tion D = S, S' in 1-:

Note The development of data structures and algo­ rithms for polynomial unification can be viewed as the attempt to achieve the polynomial time step-reliability of deduction systems using unification.

Unfortunately, polynomial time step-reliability is not sufficient for guaranteeing polynomial transparency. Ad­ ditionally, a size increase condition is needed. The fol­ lowing very general one will do.

Definition 4 [Logarithmic polynomial size step-reliability] A transition relation 1- is called logarithmic polynomial size step-reliable, or just logp size step-reliable, if there is an integer b > 1 and a polynomial p such that for every pair (S, S'} E 1- :

The follow~ng proposition (a proof can be found in [Letz, 1993]) is fundamental for the theory of abstraction modulo polynomials.

Proposition 1 If a transition relation 1- is polynomial time step-reliable and logp size step-reliable, then 1- is polynomially transparent.

2.5 Weak Polynomial Transparency

There are transition relations for which polynomial transparency cannot be guaranteed for arbitrary deriva­ tions, so that not in any case the input size and the steps of a derivation give a representative measure of its complexity. But, one may argue, when the indetermin­ istic power of the transition relation defined by a logic calculus is concerned, then it is legitimate to consider solely those derivations which are shortest proofs of the inputs. The question is how to define 'short', in terms of elementary computing cost, in terms of derivation size, or number of steps. Also, the shortest proof, in anyone of these models, may violate the condition of polynomial transparency, but the second shortest may fit. In order to facilitate the formulation of reasonably tolerant gener­ alizations of polynomial transparency, we define minimal proofs with respect to polynomials.

Definition 5 [p-(step-)minimal proof] Given a proof re­ lation 1- and a polynomial p. A proof D of an input state S in 1- is said to be p-minimal in 1- if for any proof D' of Sin 1-:

and D is called p-step-minimal in 1- if for any proof D' of Sin 1-:

Now, polynomial difference in complexity poses no problems, not the absolutely shortest proof must be taken, any proof will do which p-simulates the shortest one. Using p-step-minimal proofs the notion of polyno­ mial transparency can be weakened as follows.

Definition 6 [Weak polynomial (step-)transparency] A proof relation 1- is called weakly polynomially step­ transparent or just weakly polynomially transparent if there are polynomials p and p' such that for every in­ put state S there exists a p-step-minimal proof D of S in 1- with

Note One could even be more liberal and only demand the existence of p-minimal proofs in the definition above. We think that the resulting notion would become too weak, for the following reason. With the notion of weak polynomial transparency we intend to express that the abstraction level of inference steps indeed provides a rep­ resentative complexity measure for the indeterministic power of a proof relation, even though not for the ab­ solutely shortest proofs, so at least for one of the short proofs. But the class of short proofs should be defined in terms of inference steps, this way demonstrating the usefulness of the abstraction level.

3 Transparency Properties of Resolution

As a typical representative of a logic calculus relying on the use of lemmata, we shall study the transparency properties of the resolution calculus. 5 The resolution cal­ culus [Robinson, 1965] can be formulated as a system of a single but complex inference rule of the shape

where 0 is a most general unifier for the set of atomic formulae {Al, ... ,Am,Bl,···,Bn}, and r1 and r2 are clauses; implicitly assumed is the renaming of the vari­ ables in one of the input clauses of the rule.

Let us illustrate at this example the distinction be­ tween the declarative and the process interpretation of a deduction. While a deduction of the former type is sim­ ply a sequence D of clauses where each element of D is either from the input set or derived from earlier elements of D, the deduction process consists of a sequence of in­ creasing clause sets. If the deduction process is based on unrestricted resolution-which is free of reduction rules like subsumption deletion-, then any state of the deduc­ tion process is just a deduction of the declarative type. This property holds for all calculi which are accumula­ tive. 6

5 The transparency properties of other calculi are studied in [Letz, 1993].

6 ln general, however, the states of a deduction process need not represent declarative deduction objects, even if no reduction rules, like subsumption deletion, are applied. This example also exhibits a certain disadvantage of measuring the size of a deduction as the sum of the sizes of the states

3.1 Resolution and Polynomial Transparency

While polynomial size-transparency can be guaranteed for resolution-provided polynomial unification algo­ rithms are used-, it is evident that resolution is not polynomially transparent .

Proposition 2 Resolution for first-order logic is not polynomially transparent.

Proof Consider the following formula F consisting of three clauses 7 of the shape

where 0 denotes a constant. By performing self­ resolution on the second clause co of F and then repeat­ edly applying self-resolution to the deduced resolvents, in k steps one can generate a clause Ct of size > 2t. From Ct the empty clause can be deduced in two fur­ ther resolution steps. Clearly for any polynomial p there exists a proof D = D1, . . . , Dm of this type such that size( D) > p{size(F), m), that is, the size of D cannot be bounded by any polynomial on the size of the input formula and the number of resolution steps. 0

Consequently, in contra8t to propositional logic, for first-order logic the number of resolution steps is not an adequate measure for the complexities of resolution derivations and proofs. The apparent reason is the fol­ lowing. Due to the renaming of derived clauses, resolu­ tion violates the logp size step-reliability. 8

But one may object that a resolution proof of the spec­ ified type is not an optimal one, and that there exists a shorter resolution proof for F which immediately de­ rives the empty clause, by simply resolving the two facts ....,p(z) and P(O) . For this short proof the relation be­ tween the proof size and the proof steps is polynomial modulo the input size.

3.2 Resolution and Weak Polynomial Transparency

The question is now whether for shortest resolution proofs the sizes and the inference steps are always poly­ nomially related, or in our terminology, whether weak polynomial transparency can be guaranteed for resolu­ tion. Unfortunately, the answer to this question is no, too. There is an infinite formula class for which every resolution proof is exponential in size with respect to the input formula, whereas there are proofs that get by on polynomially many resolution steps.

The next example specifies a formula class with this property. Assume in the following that, for any 1 ~ i ~

in the deduction process, since untouched parts of the states are counted multiply. A finer model would count only the touched parts of the non-initial states.

7 For reasons of readability, we prefer to write clauses as disjunctions of literals; furthermore, we use the term 'for­ mula' for sets of clauses.

8 lt should be emphasized that the reason is indeed the renaming of derived clauses and not their multiple use as parent clauses.

n, ~~ is the value of the i-th prime number, and that s"(z) abbreviates a term of the structure s(- · · s( z) · · ·). ....___.... k-times

Example 2 For any positive integer n, let Fn denote a Horn formula consisting of the following structure:

If in this class of Horn formulae the function symbol s is interpreted as the successor function, and if the de­ notation of a predicate P; is the set of natural numbers divisible by the i-th prime number, then such a formula can be used to compute common multiples of primes. Apparently, from these considerations we can derive the following lemma.

Lemma 3 Given a formula Fn of the type specified in Example 2, let c () be any ground instance of the first clause c E Fn such that (Fn \ { c}) U { c 0} is unsatisfiable. Then the largest occurring term in c () must denote a common multiple of the first n prime numbers.

Since the least common multiple of a sequence ~1 ' ... '~n of primes equals n~=l ~.' the following ob­ vious result gains importance.

Lemma 4 There is no polynomial p such that for every positive integer n:

An immediate consequence of this result 1s that n~=1 ~. cannot be polynomially bounded by the size of the input formula Fn.

Lemma 5 There is no polynomial p such that for every positive integer n : p(size(Fn)) > TI~=t ~~ ~ where Fn is a formula of the type specified in Example 2.

The formula class described in Example 2 is in­ tractable for resolution.

Proposition 6 There is no polynomial p such that for every positive integer n : p(size(Fn)) is greater than the size of any resolution refutation for Fn.

In the proof of this proposition we shall exploit the fact that the formula class in question consists of Horn clause formulae, for which the following lemma holds.

Lemma 7 If t is a resolution refutation dag 9 for a Horn clause formula, then t contains one branch b­ called the negative branch -on which exactly the nega­ tive clauses of the refutation lie, i.e., those clauses which are void of positive literals.

9 A resolution dag (directed acyclic graph) is a rooted dag whose nodes are labelled with clauses such that every non­ leaf node N has two outgoing edges to nodes Nt, N2, and the clause at N is a resolvent of the clauses at N1 and N2. A resolution refutation dag is a resolution dag whose root is labelled with the empty clause.

Proof of Lemma 7 It suffices to notice that, on the one hand, in such a dag no non-negative clause can dom­ inate a negative clause, and, on the other hand, every negative clause must be derived from a negative and a non-negative clause.

Proof of Proposition 6 Let t be an arbitrary reso­ lution refutation dag for a formula Fn, and let b be the negative branch oft, which exists by Lemma 7. Clearly, each occurrence of a negative clause on b is used only once as a parent clause in t. Consequently, replacing all clauses on the branch b by appropriate ground instances does not alter the length of the branch, while the result­ ing dag remains a refutation-of resolution with free, i.e., not necessarily most general, unification rule. If this par­ tial instantiation is performed on t, the negative branch b' of the resulting refutation dag t' must contain ground instances

of the first clause c E Fn . Let co, ... , Ck be the clauses on the initial segment of the branch b' from the root labelled with co (the empty clause) up to the first in­ stance CJc of c. Obtain t 11 by making Ck a leaf oft' (it may already be one) plus removing the nodes and edges which are no more accessible from the root. Apparently, t 11 still remains a refutation dag. Since CJc is the only instance of c in t 11 , (Fn \ {c}) U {c~c} must be unsat­ isfiable. From Lemma 3 follows that in Ck the maximal term depth ~ ~ TI7:1 ~~. Consider now the non-negative clauses s1 , ... , SJc in the refutation t 11 which are resolu­ tion partners of the clauses c1, . .. , CJc respectively-let us call those non-negative clauses the side clauses. The structure of Fn guarantees that each side clause either has the form

or the form

Consequently, if ascending the branch b' by one step to­ wards the root from c; to c,_ t, 1 ::; i ::; k, the clause size can only decrease by at most the size of the respective side clause s; (disregarding the logical symbols):

Therefore,

Because size( co) = 1, and since the side clauses have not been modified by the partial instantiation operation, we get that

An application of Lemma 5 completes the proof. 0

The existence of intractable formula classes for reso­ lution is nothing exceptional, even for the propositional case (at least since Haken's work [Haken, 1985]). The special property of the formula class considered here con­ cerns the relation between the proof sizes and the num­ bers of derivation steps. Although all resolution proofs for the formula class are superpolynomial, there are short proofs in terms of inference steps.

Proposition 8 There is a polynomial p such that for every formula Fn from the class specified in Example 2 there exists a resolution refutation D1, ... , Dm of Fn such that m < p(size(Fn)).

Proof Let ~ = TI~= 1 !.p;, i.e., the least common multiple of the primes !.p1 , ... , '.Pn. Then a polynomial-step proof can be constructed as follows. For every clause of the type

perform self-resolution and repeatedly apply self­ resolution to the respective resolvents. Within k steps this operation deduces clauses in which the number of occurrences of the function symbol s in the positive lit­ erals successively takes the values !.p; 2 1 , !.p; 2 2 , . . . , !.p; 2A:. This is done as long as !.p; 2A: ~ ~. Then, after at most k further resolution steps which use clauses from this derivation, each clause at most once, a formula of the structure

can be deduced. Accordingly, for any 1 ~ i ~ n, we need at most 2log2 f steps, which is less than 2log2 ~, hence for all i : less than 2n log 2 ~. Lastly, in further 2n resolu­ tion steps the empty clause can be derived by resolving these clauses with the facts and the resulting n facts P;(se(o)), 1 ~ i ~ n, with the first clause. The whole refutation takes less than 2n + (2n log2 ~) ~ 4n log2 ~ steps. It remains to be shown that this value is polyno­ mially bounded by the size of Fn . For this purpose we may just use ( = L:~1 !.p; as a lower bound for the size of Fn and consider the chain

The first inequality holds because of properties of the arithmetical mean, while the others are trivial. 0

The Propositions 6 and 8 have as an immediate con­ sequence that, even if only step-minimal proofs are con­ sidered, the number of steps of a resolution proof may not be a representative measure for the complexity of the proof.

Theorem 9 Resolution for first-order logic is not weakly polynomially transparent.

The violation of the logp size step-reliability turns out to be fatal, even if only short proofs are counted.

3.3 Methods for Obtaining Polynomial Transparency

The situation is quite instructive, because we can illus­ trate at the example of resolution the three principal solution methodologies when facing the polynomial in­ transparency of a transition relation 1- .

The first approach is to weaken the transition relation 1- and to define a transition relation 1-', for example, by taking out each pair (S, S'} which violates the logp size step-reliability, since this may be the problematic property, like in the case of resolution. The most radical method to perform this modification on the resolution calculus is to forbid the renaming or even the multiple use of lemmata. The latter results in the calculus of tree resolution. Tree resolution is polynomially transparent, even in the strict sense (a proof can be found, e.g., in [Eder, 1992] or in [Letz, 1993]). But unfortunately, this has the unacceptable consequence that many proofs are thrown out which are short in steps and small in size.

Also, eliminating problematic pairs from a transition relation does not work for arbitrary transition relations. This leads to the second alternative. In order to pre­ serve the problem solving functionality of the relation, that is, to guarantee that the transitive closures-or at least the provable states-of both transition relations re­ main identical, in the general case, each problematic step must be replaced by a series of computationally innocu­ ous steps. For logic calculi, this amounts to a redefinition of the notion of an inference step.

Both methods are relatively unappealing for the prac­ tical working with logic calculi, since in no case the in­ deterministic power of a calculus is increased, either it is weakened or it remains unchanged, and only the pre­ sentation structure of the calculus is modified.

The real importance of the notion of polynomial trans­ parency for the advance of science is that it can moti­ vate research following the third approach. The third approach is to let the general structure of a transition relation as it is, and to try to remedy the polynomial in­ transparency of the transition relation. Since the typical stumble-block for attaining polynomial transparency is the violation of the logp size step-reliability, a promising research direction consists of improving the data struc­ tures of the elements in the transition relation in such a way that they can be represented with less space than in the original relation, with the hope to gain polyno­ mial transparency this way. The advantage of such an attempt, if it succeeds, is that the distances between the elements in the transition relation can be preserved while the real computing cost and sizes properly decrease.

The difference between the solution methodologies is that the second approach always succeeds, whereas the third one may fail in principle. 10

3.4 Improvements of the Representation of Formulae

Similar to the case of the unification operation, which, in order to attain the polynomial time step-reliability of an inference system, has enforced the necessity to represent logical terms as dags, one should think about the devel­ opment of more sophisticated mechanisms which would admit a notation for resolvents polynomially bounded in size by the number of their derivation steps, with respect to the input formula.

10 Such an impossibility result for resolution is proven in [Letz, 1993]. There it is shown that there can be no data structure for achieving the strong polynomial transparency of resolution, if not the factoring rule is modified. This result indeed enforces a redefinition of the resolution inference step.

An obvious improvement is to integrate into the ob­ ject language the same vocabulary of upper indices we already used in our meta-language for the purpose of polynomially specifying terms of exponential depth. It is apparent that with the use of such number terms the transparency problems of the Examples 1 and 2 can be solved, even polynomial transparency in the strong sense can be achieved for these examples. One can predict that number terms will play an important role in future au­ tomated deduction systems. 11

We shall not pursue further the attempt of extending the representation of logical formulae, instead we want to present a critical example class which may turn out to be a hard problem for the efforts to achieve polynomial transparency. These new formulae are obtained from the previous class of Example 2 by augmenting the arity of the function symbol s by 1. This means that the previous formula class is just an abstraction of the new class.

Example 3 For any positive integer n, let Fn denote a Horn formula of the following structure:

In the new class the second argument of the function symbol s does not play any role at all, the variables at these positions are just dummy variables. Conse­ quently, the results concerning proof steps and proof lengths carry over from Example 2 to this example. But there is a crucial difference between both examples, which becomes apparent when self-resolution is applied to a clause of the mixed type in Example 3. Let us demonstrate this with the input clause corresponding to the prime number 3:

In its self-resolvent

the number ·of distinct dummy variables has doubled. In general, in any such self-resolution step the resolvent contains 2n - 1 more distinct variables than the orig­ inal clause. Accordingly, for this class of formulae, in any polynomial-step proof of an instance Fn, clauses are needed in which not only the term depth is exponen­ tial (which could be remedied by using number terms in the object language) but also the number of distinct variables. And to this problem no obvious solution is in sight. 12

11 Much more than polynomial unification algorithms, which have turned out to be relatively unimportant for the practice of deduction systems. This can be verified by observ­ ing that the examples (particularly Example 1) for demon­ strating the necessity of number terms are much simpler and occur more frequently in practice than the ones which de­ mand polynomial unification techniques.

Conclusion and FUrther Research

This paper has illustrated that a formalization of intu­ itively existing abstraction concepts for logic calculi can be very fruitful. The developed notion of polynomial transparency promises to serve as a useful and research­ stimulating property of deduction systems, and of tran­ sition relations in general. The main technical result of this paper is the demonstration that the number of inference steps of resolution proofs do not give a repre­ sentative measure of the actual proof complexities, even if only shortest proofs are considered.

As further obvious research perspectives concerning the transparency problem of resolution and other cal­ culi using the renaming of lemmata, we wish to mention the development of more sophisticated data structures than number terms; the clarification of the relation be­ tween strong and weak polynomial transparency; and finally, the study of the difficulties of rendering particu­ lar calculi polynomially transparent and the connection of these difficulties with certain problem classes in the polynomial ~ierarchy.