Strategies in Rigid-Variable Methods

1 Introduction

Automated reasoning methods for first-order classical logic can generally be divided in two classes.

Methods of the first class use universal variables (res­ olution [Robinson, 1965], the inverse method [Maslov, 1983]). Variables in these methods are local to a clause (formula, sequent) and can be considered as univer­ sally quantified in this clause (respectively formula or sequent) . [Maslov et al., 1983; Maslov, 1987] charac­ terized these methods as local methods (see also [Mints, 1990]). .

Methods of the second class use rigid variables (the tableau method [Beth, 1959], the mating or the con­ nection method [Andrews, 1981; Bibel, 1981], model elimination [Loveland, 1968], SLD-resolution [Kowalski, 1974; Apt and van Emden, 1982], SLO-resolution [De­ molombe, 1989; Rajasekar, 1989]). Variables in these methods are local to a set of clauses (formulas, sequents) and can be considered as universally quantified in this set of clauses (respectively formulas or sequents). [Maslov et al., 1983; Maslov, 1987] characterized these methods as global methods. In this paper, we shall call such methods rigid-variable methods.

Both kinds of methods have their advantages and dis­ advantages which are well-known. There are papers comparing resolution and tableau-like calculi, for exam­ ple [Eder, 1988; 1991] (see also [Bibel and Eder, 1993]).

*Computing Science Department, Uppsala University, Box 311 S-751 05 Uppsala, Sweden. Supported by a TFR grant. URL page: http:/ /www.csd.uu.se;-voronkov. Email: voronkov@csd. uu.se.

Recently, there have been proposals combining both kinds of methods in one calculus, fo,r example the equal­ ity elimination method [Degtyarev and Voronkov, 1995b; 1995a; 1996a] or a modification of model elimination [Moser et al., 1995].

Although there are many implementations of rigid­ variable methods, there are almost no papers investigat­ ing the intrinsic complexity of problems arising in rigid­ variable methods. In this paper we study several com­ plexity problems related to rigid-variable methods on a decidable fragment of predicate calculus with equality. We show that the use of such methods can introduce es­ sential complications even for this relatively simple frag­ ment . We also demonstrate that methods with rigid vari­ ables can gain from the intelligent use of strategies for multiplicity. In addition, we show that a recent result of [Voda and Komara, 1995] on the Herbrand skeleton problem is related to an inadequate formulation of the problem, and pose a new open problem.

2 Preliminaries

A term or atomic formula is ground iff it has no variables. The symbol f- denotes provability in first-order logic. When we write <p1, . . . , <pn f- <p , where <p1, . .. , <pn, <p are formulas, it means provability of the formula <p1 1\ . . . 1\ <pn :) <p. Substitutions of terms t 1 , . ·. , tn for variables x1 , . .. , Xn are denoted { ttf X1, ... , tn/ Xn}. The applica­ tion of such a substitution B to a term t, is the operation of simultaneous replacement of all occurrences of x; by t;. The result of the application is the term denoted tB. We shall also apply substitutions to formulas, equations and sets of equations and use the same notation for the result of the application.

We shall consider first-order predicate logic with equality. The equality predicate is denoted by -:::: , in order to distinguish it from the metasymbol = used to denote the identity of two expressions . The symbol ;:= means "equal by definition". Atomic formulas s -:::: t are called equations, and their negations ...,s -:::: t , denoted s 'f. t, disequations. We do not distinguish an equation s -:::: t from the equation t -:::: s. For a technical convenience, we can also use equations and disequations between atomic formulas, for example P(s1, ... , sm) -:::: Q(tl, ... , tn)·

1. Choose a positive integer f..l·
2. Construct the formula 'P~-t = (cp(x1) V ... v cp(xl-')) and check whether there is a substitution () such that the formula 'P~-t() is provable.
3. If such a substitution exists, then the goal formula 3xcp(x) is provable. Otherwise, increase f..l and come back to step (2).

Figure 1: a'he Procedure: a typical procedure for rigid­ variable methods

Let s1, t1, ... , sn, tn, s, t be terms. We write s1 ~ t1, . . . , Sn ~ tn 1- s ~ t to denote that the formula V( s1 ~t1 1\ ... . 1\ Sn ~tn :::::> s~t) is true, i.e. it is prov­ able in first-order logic. Equivalently, we can say that s and t lie in the same class of the congruence generated by {sl~tl>·· · ,Sn~tn}·

A rigid equation is an expression [ 1-v s~t, where [ is a finite set of equations. [ is called the left hand side of this rigid equation, and the equation s ~ t - its r·ight hand side. A solution to a rigid equation { s1~t1, ... , Sn~tn} 1-v s~t is any substitution a such that s1a ~ t1a, ... , Sna ~ tna 1- sa ~ ta. A system of rigid equations is a finite set of rigid equations. A solution to a system of rigid equations R is any substi­ tution that is a solution to every rigid equation in 7?. The problem of solvability of rigid equations is known as rigid E-unification. The problem of solvability of sys­ tems of rigid equations is known as simultaneous rigid E-unification, or SREU for short.

We shall denote sets of equations by [ , systems of rigid equations by R and rigid equations by R. We shall sometimes write the left hand side of a rigid equation as a sequence of equations, for example x~a 1-v g(x)~x instead of {x~a} 1-v g(x)~x.

For simplicity, in this paper we consider the provabil­ ity problem for closed prenex ·existential formulas, i.e. formulas of the form 3xcp(x), where cp(x) is a quantifier­ free formula. There is a provability-preserving poly­ nomial time translation of arbitrary formulas to closed prenex existential formulas by means of Skolemization and prenexing.

According to the Herbrand theorem, such a formula is provable if and only if there exists a positive in­ teger f..l and a substitution () such that the formula (cp(xi) V ... V cp(x 1 ,))B is provable. This fact is used in several automated reasoning methods, for example in the method of matings, in the way shown in Figure 1. The procedure shown in that figure will simply be called the Procedure.

In the method of matings, before step (2) the formula cp 1 , is represented in the form of a matrix M and the provability of cp 1 ,() means that any vertical path in MB is inconsistent. The tableau method represents the formula in the form of a tree and uses branches of the tree instead of vertical paths.

The number f..l used in the Procedure (the number of copies of cp(x) which can be used) is usually called mul­ tiplicity. Of course, there are various modifications of the Procedure, for example, the goal formula may be non-prenex. In this case the notion of multiplicity is more complicated. Our results can also be generalized to more complex notions of multiplicity. However, we shall only consider prenex existential formulas, for which the notion of multiplicity is defined as a positive integer number.

We informally call a strategy for multiplicity any pro­ cedure which selects the initial multiplicity and increases multiplicity in the Procedure. The standard strategy for multiplicity is the strategy which sets f..l initially to 1 and increments it by 1 on any further step. A strategy for multiplicity is called formula-independent iff it does not depend on the input formula.

There are various algorithms for checking, for a given formula 'P~-t, whether there is a substitution making this formula provable. Instead of studying concrete proce­ dures, we shall study the intrinsic complexity of the problem which can be formulated as follows.

Problem 1 (Herbrand Skeleton) Given a quantifi­ er-free formula cp(x) and a positive integer f..l, are there term sequences f1, ... , tn such that the formula cp( [1) V .. . V cp(t 1 ,) is provable?

[Degtyarev et al., 1996a] give an informal survey of several decision problems arising from the Herbrand the­ orem, including the Herbrand Skeleton problem. It is clear that Problem 1 is decidable if and only if the fol­ lowing problem is decidable.

Problem 2 (Formula Instantiation) Given a quan­ tifier-free formula cp(x), is there a term sequence [such that the formula cp( f) is provable?

Note that the formula instantiation problem is repeat­ edly used in the procedures used by the method of mat­ ings or the tableau method.

The decidability of these problems is equivalent to the decidability of SREU. Unfortunately, it turned out that SREU has almost no decidable fragments which are gen­ eral enough. Some known results on SREU are the fol­ lowing.

• SREU is undecidable [Degtyarev and Voronkov, 1996b].
• SREU with ground left hand sides is undecidable [Plaisted, 1995].
• SREU with ground left hand sides and two variables is undecidable [Veanes, 1996].
• SREU with one variable is DEXPTIME-complete [Degtyarev et al., 1997].

The case of one variable is hardly useful in automated reasoning. When all function symbols have arity ::; 1, Formula Instantiation is equivalent to monadic SREU, i.e. SREU in the signature where all function symbols have arity :S 1. The decidability of monadic SREU is an open problem. The following facts are known about monadic SREU.

• Monadic simultaneous rigid £-unification with one function symbol is decidable (this fact has a rather non-trivial proof in [Degtyarev et al. , 1996b]).
• Monadic simultaneous rigid £-unification with more than one function symbol is equivalent to a non­ trivial extension of word equations [Gurevich and Voronkov, 1997a].

Some other decidable fragments of monadic SREU are considered in [Gurevich and Voronkov, 1997a], but they are hardly of much use for automated reasoning.

Since predicate calculus is undecidable, the undecid­ ability of SREU does not add much to the complexity of predicate calculus. In this paper we consider the behav­ ior of methods based on rigid variables on a decidable fragment of predicate calculus.

3 Ground-negative fragment of predicate calculus

A formula cp is called positive if all atomic subformulas of cp are positive. A closed formula cp is ground-negative iff any occurrence of a variable in cp is either an occurrence in a positive atomic subformula of cp or is bound by an essentially universal quantifier (i.e. an universal quanti­ fier occurring in cp positively or an existential quantifier occurring in cp negatively?. [Kozen, 1977] proves the following result.

Theorem 1 The class of provable formulas of the form A1 1\ ... 1\ An :::> cp, where A1, ... , An are ground atomic formulas and cp is a positive formula, is NP-complete.

Using this result, one can prove the following:

Theorem 2 The provability problem for ground-negati­ ve formulas is in II~.

Since we only consider prenex existential formulas, such a formula 3xcp(x) is ground-negative if and only if all negative atomic subformulas of cp(x) are ground. So we consider the Herbrand skeleton problem and the formula instantiation problem for ground-negative formulas. We assume that 3xcp(x) is a fixed ground-negative existential prenex formula.

Theorem 3 The formula instantiation problem for gro­ und-negative formulas is undecidable.

Proof. We shall use the result proved in [Plaisted, 1995] that SREU with ground left hand sides is undecidable. Consider any system R of rigid equations with ground left hand sides:

1 Variables occurring in essentially universal quantifiers can also be characterized as eigenvariables. Thus, a formula cp is ground-negative if and only if every variable occurring in a negative atom in cp is an eigenvariable.

Consider also the following formula cp:

It is straightforward that a substitution e is a solution to R if and only if the formula cpB is provable. Note that all negative atoms in cpB are ground. Hence, SREU with ground left hand sides is effectively reducible to the formula instantiation problem for ground-negative formulas. Thus, the formula instantiation problem for ground-negative formulas is 'undecidable. 0

If we consider which systems of rigid equations arise from ground-negative formulas (e.g. according to the procedures of [Gallier et al., 1990; 1992]), we shall find out that these are precisely all systems of rigid equations with ground left hand sides.

Theorem 3 shows that a straightforward use of rigid­ variable methods can create unnecessary complications, for example, the necessity to solve an intermediate un­ decidable subproblem in order to solve a problem in II~. This theorem can be reformulated as a statement about the standard strategy for multiplicity:

Theorem 4 For the standard strategy for multiplicity, a subproblem arising at step {2) of the Procedure is un­ decidable for the class of ground-negative formulas.

Proof. Indeed, the subproblem with f.l = 1 arising at the first iteration of the algorithm is equivalent to the formula instantiation problem which is undecidable by Theorem 3. 0

Hence, the use of the standard strategy may introduce unnecessary complications into rigid-variable methods. We can prove that the same holds for arbitrary formula­ independent strategies. To this end, we shall use a result proven in [Veanes, 1997]. First, we cite a result by [Voda and Komara, 1995] which generalizes the undecidability of SREU.

We call a specialization of the Her brand skeleton prob­ lem for any fixed f.l the following problem 2 :

Given a quantifier-free formula cp(x), are there term sequences t1 , ... , til such that the formula cp(ti) V ... V cp(l,,) is provable?

The following result is proved in [Voda and Komara, 1995]:

Theorem 5 The specialization of the Herbrand skeleton problem for any fixed f.l is undecidable.

This result has recently been improved in [Veanes, 1997], where they have shown that it also holds for ground-negative formulas:

2 The Herbrand skeleton problem described in [Voda and Komara, 1995] is precisely this specialization.

·, Theorem 6 The specialization of the Herbrand skele­ ton problem for ground-negative formulas and any fixed multiplicity 1-L is undecidable.

Theorem 4 about the standard strategy for multiplic­ ity can be generalized as follows .

Theorem 7 For any formula-independent strategy, a subproblem arising at step (2) of the Procedure for the class of ground-negative formulas is undecidable.

Proof. Since the strategy is formula-independent, some J.t independent of the input formula will be selected at the first iteration of step (2). Then continue similar to the proof of Theorem 4 but using Theorem 6 instead of Plaisted's result. 0

We shall consider an intelligent strategy for multiplic­ ity in Section 4.

4 The Herbrand Skeleton Problem and intelligent strategies for multiplicity

Intelligent strategies for multiplicity have always been considered of paramount importance for rigid-variable methods. However, essentially no formal results are known about such strategies. Existing systems based on rigid-variable methods use some heuristic methods for incrementing multiplicity and universal variables when­ ever possible (see e.g. [Hahnle et al., 1994]). In this sec­ tion we show that there is an efficient formula-dependent strategy for multiplicity for the class of ground-negative formulas.

In this section 'ljJ = 3xcp( x) will denote a fixed ground­ negative existential prenex formula. Let A1 , ... , An be all its negative atomic subformulas. Denote by N the set of all subsets of {1, ... , n}. Introduce 2n sets of ground atoms £1 ;::::: {A; I i E I}, for every IE N. Using trans­ formations similar to those used in the conjunctive nor­ mal form translation, we can assume that cp(x) has the form

where cp 1 are formulas constructed from atomic formulas using /\, V. Without loss of generality we can assume that for every I, J , if J ~ I, then 1- cp 1 :::::> cp J . Indeed, if this is not true, we can replace cp 1 by cp 1 1\ cp J , then 'ljJ will be replaced by an equivalent formula.

The notion of the least Herbrand model of a set of formulas is standard and can be found in e.g. [Lloyd, 1987] or [Apt, 1990].

Lemma 4.1 Let 2t be a set of ground atomic formu­ las and cp be a closed formula constructed from atomic formulas using only 1\, V and 3. Let 001 be the least Her­ brand model of 21. If 001 ~ cp, then 2t 1- cp .

Proof. Straightforward, by induction on cp.

0

A more general variant of Lemma 4.1 also holds, where 2l is a set of universal quasy-identities (see [Makowski, 1986] or [Sheperdson, 1988]).

Lemma 4.2 Let 1- '1/J. Then for every IE N there is a substitution () such that £1 1- cp 1().

Proof. Denote by 0011 the least Herbrand model of £1. We have 0011 ~ '1/J. Since 0011 is a Herbrand model, we have 0011 ~ cp(x)B for some substitution () making all variables in x ground. We prove that () satisfies the claim.

Indeed, we have 0011 ~ (1\iEI A;) :::::> cpJ(). Since 0011 ~ (1\iEI A;), we have 0011 ~ cpJB. By Lemma 4.1 we have tJ 1- cp[(). 0

For every I E N, we denote by () 1 some substitution satisfying Lemma 4.2.

Proof. Let 001 be an arbitrary model. Consider I ~ {i I 001 ~ Ai}· Since 001 ~ 1\iEI A;, by Lemma 4.2 we have 001 ~ cp 1() I· Consider an arbitrary J E N. Let us prove that 001 ~ (1\iEJ Ai) :::::> cpJ()J. Consider two cases:

1. J ~ I . Then we have 1- cp1 :::::> cpJ. It follows that 1- cpi()J :::::> cpJ()J. Hence, 001 ~ cpJB1.

2. J% I . By the choice of 001 we have 001[;t: 1\;u A;.

In both cases we have 001 ~ (1\ iEJ A;) :::::> cpJBJ. Since J was arbitrary, we have

i.e. 001 ~ cp(x)B 1.

Then we have 001 F= V l EN cp(x) () 1. Since 001 is arbitrary, we have 1- V lEN cp(x)() I . 0

Theorem 9 The following problem is in II~ (compare it with the Herbrand Skeleton problem).

Given any ground-negative formula 3xcp(x) and any positive integer 1-L ~ 2n, where n is the number of neg­ ative atomic subformulas of cp(x), are there term se­ quences t1 , ... , tl-' such that the formula cp(t1)V ... Vcp(tl-') is provable?

Proof. By Theorem 8, if the formula 3xcp(x) is provable, then such term sequences t1 , ... , t~-' exists. Obviously, the converse is also true. Hence, the problem defined in the theorem is polynomial-time equivalent to the prov­ ability problem for ground-negative formulas. By The- · orem 2, the provability problem for such formulas is in II~ . o

Thus, for ground-negative formulas we have an inter­ esting phenomenon. For small values of multiplicity 1-L the Procedure should solve an undecidable subproblem at step (2) ; for large enough values of /-L , this subproblem is in II~. Thus, we have formally shown that for the class of ground-negative formulas, formula-dependent strate­ gies for multiplicity can result in a huge gain in efficiency.

Theorem 9 also shows that the result of Voda and Komara is not related to formula-dependent strategies for multiplicity. In order to formally define a formula­ dependent strategy, we can represent the value of f.L on the nth iteration of the Procedure as a function f of two arguments: the input formula 3x<p(x) and the number n. Since J.L should be increased with each next iteration, we have f(3x<p(x), n + 1) > f(3x<p(x), n).

Then we can formally define a strategy for multiplicity as any function f such that

1. The first argument of f ranges over prenex existen­ tial formulas 3x<p(x);
2. The second argument of f ranges over positive in­ tegers;
3. for every positive integers k > m and every prenex existential formula 'ljJ we have f('I/J, k) > f('l/J, m).

The following problem arises:

Problem 3 Is there a strategy for multiplicity f such that

1. f is computable;
2. The following problem is decidable. Given a number k and a prenex existential formula 3x<p( x), are there term sequences [1 , ... , t1(3x<p(x),k) such that the for­ mula <p(t!) V ... V <p(tf(3x<p(x) ,k)) is provable?

This problem is still open. We conjecture that such function does not exist, but the proof of this fact would require some non-trivial diagonalization.

Even if this problem has a negative solution, there are still at least two known ways for the use of rigid-variable methods for logic with equality. One way is to augment rigid-variable methods by universal-variable parts, as for example in [Degtyarev and Voronkov, 1995b; 1996a] or [Moser et al., 1995]. Another way is to use incomplete but terminating algorithms on step (2) of the Procedure, as demonstrated in [Plaisted, 1995] or [Degtyarev and Voronkov, 1996c].

Acknowledgments

I thank Anatoli Degtyarev, Yuri Gurevich and Margus Veanes. Some ideas of this paper appeared as a result of our discussions. I thank an anonymous referee who pointed out serious inaccuracies in the preliminary ver­ sion of this paper.