Strong Skolemization

Andreas Nonnengart^{∗} Max-Planck-Institut für Informatik and Saarbrücken University Im Stadtwald, 66123 Saarbrücken, Germany

Abstract

Skolemization is a means to eliminate existential quantifiers within predicate logic sentences by replacing existentially quantified variables with Skolem function applications. The arguments of such Skolem functions are variables that are quantified outside the sub-formula under consideration. In this article a skolemization technique is introduced which abstracts from some of the Skolem function arguments. It turns out that the result obtained this way is usually more general than what can be achieved from standard (classical) Skolemization techniques. From a theorem prover’s point of view such generalizations often lead to a reduction of both search space and proof length.

1 Introduction

In automated theorem proving much effort is spent on the development of more and more sophisticated reasoning calculi whereas the optimization of certain normal form transformations as they are, for example, necessary for resolutionbased theorem proving, are fairly neglected.

One part of the usual clause normal form transformation for resolution is Skolemization (See the historical paper (Skolem 1920)). Its major effect lies in substituting so-called Skolem function applications for existentially quantified variables. Usually, there are two kinds of Skolemization techniques mentioned in the standard literature on automated theorem proving^{1} which we call Inner and Outer Skolemization in this paper. The two differ mainly in the choice of the arguments for the Skolem functions (see below).

Strong Skolemization, as it is introduced here,^{2}b can be viewed as a generalization of Inner Skolemization in the sense that some of the Skolem function arguments are replaced with new (universally quantified) variables. This often allows for considerable simplifications after generating normal forms for automated theorem proving and therefore leads to a reduction of both search space and proof length.

∗Andreas.Nonnengart@mpi-sb.mpg.de, http://www.mpi-sb.mpg.de/˜ nonnenga/

1see, e.g., (Loveland 1978, Chang and Lee 1973)

2A slightly less general version appeared in (Nonnengart 1996)

This article is organized as follows: First, the standard notion of Skolemization is recapitulated. Then the new Strong Skolemization technique is introduced which, finally, is to be compared with another, somewhat related, method developed recently, the so-called Optimized Skolemization.

2 Preliminaries

For simplicity, we assume formulas to be in negation normal form^{3} and that any two different quantifiers inside a formula bind variables with different names. This is to ensure that the occurrence of a sub-formula ∃x Φ or ∀x Φ in a given formula Δ is unique.

By Δ [Φ] we indicate that Φ is a sub-formula of Δ and Δ [Φ / Ψ] is a representation of Δ with sub-formula Φ replaced by Ψ.^{4}

We refer to the set of free (i.e. not bound by any quantifier) variables in Φ by V(Φ). For any variable x occurring in Δ, the (unique) sub-formula starting with the quantifier which binds x is referred to by Δ^{x}. Thus, if ∃x Φ is a sub-formula of Δ then Δ^{x} = ∃x Φ.

For readability we abbreviate sequences of the form u_{1}, …, u_{k} of length k by \overline{u}_{k}.

A (first-order) interpretation M = (D, ℑ, ϕ) consists of a non-empty domain of discourse D, a mapping ℑ which associates functions and relations to function symbols and predicate symbols respectively, and a variable valuation ϕ which maps variables to elements of D. Given a valuation ϕ we mean by ϕ[x/d] the variable valuation that is identical to ϕ except for the variable x which is to be interpreted as the domain value d. Similarly, by M[x/d] we understand the triple (D, ℑ, ϕ[x/d]) provided M = (D, ℑ, ϕ). Moreover, we use ϕ[\overline{x}_{k}/\overline{α}_{k}] as short for ϕ[x_{1}/α_{1}][x_{2}/α_{2}] ⋯ [x_{k}/α_{k}].

Finally, whenever we write Φ{x/t} we mean Φ with every occurrence of the (free) variable x replaced by the term t.

Definition 2.1 (inner and outer skolemization) We obtain the Skolemization of a sentence Δ by replacing every occurrence of sub-formulas ∃x Φ in Δ with a corresponding Φ\{x/f(\overline{y}_{n})\}, where f is an nplace function symbol which is new to the problem under consideration. We speak of Outer Skolemization in case the variables \overline{y}_{n} are all the universally quantified variables such that ∃x Φ is a sub-formula of Δ^{y_{i}} for each 1 ≤ i ≤ n.

3A formula is said to be in negation normal form if it doesn’t contain implications, equivalences, and exclusive disjunctions, and all negations are moved inwards as far as possible (i.e., they only occur directly in front of predicate symbols).

4This definition won’t be ambiguous since we are only going to replace sub-formulas of the form ∃x Φ in the sequel which, under the above assumption, are unique for the formulas we consider.

If \{y_{1}, …, y_{n}\} = V(∃x Φ), i.e. the variables \overline{y}_{n} are all the free variables in the sub-formula ∃x Φ, we speak of Inner Skolemization.

Skolemization is not an equivalence transformation. It preserves satisfiability and unsatisfiability, though. This is stated in the following Lemma (proofs are omitted, for they can be found in most common textbooks and survey articles on first-order predicate logic theorem proving as, e.g., in (Chang and Lee 1973, Loveland 1978, Andrews 1981, Skolem 1920)).

Lemma 2.2 Let Δ[∃x Φ] be a sentence (in negation normal form) and let f, \overline{y}_{n} as in Definition 2.1. Then

Δ [∃x Φ] is satisfiable iff Δ [∃x Φ / Φ\{x/f(\overline{y}_{n})\}] is satisfiable

Outer Skolemization generates new Skolem functions which get all the universally quantified variables as arguments the formula under consideration depends on. There might be unnecessarily many such variable dependencies, however, if the formula to be skolemized is not in anti-prenex form.^{5} As an example consider the formula ∀x, y [∃z P (x, z) ∨ Q(x, y)] for which standard Outer Skolemization leads to ∀x, y [P (x, f(x, y)) ∨ Q(x, y)]. If preceded with an anti-prenex transformation, however, we would end up with the simpler ∀x [P (x, f(x)) ∨ ∀y Q(x, y)] instead.

For Inner Skolemization, Skolem functions are introduced which take only “necessary” variables as arguments. However, the Skolemization result depends on the order of the Skolemization of the sub-formulas. As an example consider the formula ∀x [∃y (P (x, y)∧∃z Q(x, y, z))]. If we first skolemize on ∃z Q(x, y, z) then we finally end up with ∀x [P (x, f(x)) ∧ Q(x, f(x), g(x, f(x)))] whereas starting the Skolemization with the outer existentially quantified sub-formula yields ∀x [P (x, f(x)) ∧ Q(x, f(x), g(x))]. Evidently, the latter is to be preferred. Indeed, Inner Skolemization should always be performed from left to right if we want to avoid a nesting of Skolem functions.

Note that this still does not guarantee that the least possible variable dependencies are found. For instance, consider the formula ∀x, y ∃z [P (z) ∧ (Q(x, z) ∨ R(y, z))] which, after Skolemization, gets transformed into ∀x, y [P (f(x, y)) ∧ (Q(x, f(x, y))∨R(y, f(x, y)))] and that regardless of which of the above Skolemization possibilities is performed. If we first distributed the ∧ over the ∨, however, we would be able to perform an anti-prenex step and therefore skolemize the formula ∀x, y [∃z (P (z)∧Q(x, z))∨∃z (P (z)∧R(y, z))]. In this case we would end up with ∀x, y [(P (f(x))∧Q(x, f(x)))∨(P (g(y))∧R(y, g(y)))]. Thus we have fewer dependencies for the price of having to deal with more Skolem functions. Whether or not this is still of some advantage varies from case to case; we shall not discuss this issue in this paper. The interested reader is referred to (Baaz and Leitsch 1994).

5A formula is said to be in anti-prenex form if all quantifiers are moved inwards as far as possible. There is only one exception, namely, existential quantifiers are not distributed over disjunctions. It is even the case that formulas of the form ∃x Φ[x] ∨ ∃y Ψ[y] are transformed into ∃x (Φ[x] ∨ Ψ[x]) in order to reduce the number of existential quantifiers. The value of anti-prenexing can be of quite some significance (see, e.g., (Egly 1994, Loveland 1978)) and that regardless of whether we perform Inner or Outer Skolemization.

3 The Strong Skolemization Technique

Strong Skolemization applies to sub-formulas of the form ∃ \overline{x}_{k} (Φ_{1} ∧ … ∧ Φ_{n}). Unlike in the definition of standard (Inner or Outer) Skolemization this rather general form is actually needed and cannot be simulated by several successive applications on cases of the form ∃x (Φ_{1} ∧ Φ_{2}) as will be seen in the examples to come. But before we formally define what Strong Skolemization is about let us first illustrate its behavior with the help of a little example. Let M = (D, ℑ, ϕ) be an interpretation that satisfies ∃x (P (x) ∧ Q(x, y)). The value of x may vary with the value of y, but, anyhow, we know that the set associated with the predicate symbol P, ℑ(P), is non-empty. Now let ĥ: D → D be a total function whose codomain is just ℑ(P). Then

M[x/ĥ(α)] ⊧ P (x)  for every α ∈ D and
M[x/ĥ(α)] ⊧ Q(x, y) for some α ∈ D

Therefore there exists an interpretation M′ such that

M′[x/α] ⊧ P (h(x))  for every α ∈ D and
M′[x/α] ⊧ Q(h(x), y) for some α ∈ D

where M′ which differs from M only in the interpretation of the new function symbol h which is to be interpreted as M′(h) = ĥ. Hence

M′ ⊧ ∀x P (h(x)) ∧ ∃x Q(h(x), y)

and we know by standard (Inner) Skolemization that there exists an interpretation M′′ which extends M′ only by a suitable interpretation for the new function symbol g such that

M′′ ⊧ ∀x P (h(x)) ∧ Q(h(g(y)), y)

This implies (by instantiating the variable x) that

M′′ ⊧ ∀w P (h(g(w))) ∧ Q(h(g(y)), y)

and thus finally (with M′′′(f) =^{Def} M′′′(h) ∘ M′′′(g))

M′′′ ⊧ ∀w P (f(w)) ∧ Q(f(y), y)

The sub-formula ∀w P (f(w)) ∧ Q(f(y), y) denotes the Strong Skolemization result on the original sub-formula. Notice that standard Inner Skolemization applied to the very same input would result in P (f(y)) ∧ Q(f(y), y), i.e., in a formula that is subsumed by the Strong Skolemization result; Strong Skolemization is thus more general.

Definition 3.1 (free variable splitting) Given a formula ∃ \overline{x}_{k} (Φ_{1} ∧ … ∧ Φ_{n}) let

\begin{aligned}\{\overline{z_{1}}_{l_{1}}\} & = & V(Φ_{1}) \ \{\overline{x}_{k}\} \\ \{\overline{z_{i}}_{l_{i}}\} & = & (V(Φ_{i}) \ ⋃_{1≤j<i} V(Φ_{j})) \ \{\overline{x}_{k}\} for 1 < i ≤ n \end{aligned}

We call ⟨\{\overline{z_{1}}_{l_{1}}\}, …, \{\overline{z_{n}}_{l_{n}}\}⟩ the free variable splitting of ∃ \overline{x}_{k} (Φ_{1} ∧ … ∧ Φ_{n}).

Intuitively, each \{\overline{z_{i}}_{l_{i}}\} contains the free variables of Φ_{i} (without the existentially quantified \overline{x}_{k}) that did not yet occur in an “earlier” Φ_{j}. Such a free variable splitting has some interesting features. So, e.g., its elements are pairwise disjoint and their overall union covers exactly the free variables of the formula ∃ \overline{x}_{k} (Φ_{1} ∧ … ∧ Φ_{n}). An important property which will be used in the sequel is the following: Whenever ⟨\{\overline{z_{1}}_{l_{1}}\}, …, \{\overline{z_{n}}_{l_{n}}\}⟩ is a free variable splitting of ∃ \overline{x}_{k} (Φ_{1} ∧ … ∧ Φ_{n}) then ⟨\{\overline{z_{1}}_{l_{1}}, \overline{z_{2}}_{l_{2}}\}, \{\overline{z_{3}}_{l_{3}}\}, …, \{\overline{z_{n}}_{l_{n}}\}⟩ is a free variable splitting of ∃ \overline{v}_{k} (Φ_{2} ∧ … ∧ Φ_{n})\{x_{i}/f_{i}(\overline{z_{1}}_{l_{1}}, \overline{v}_{k})\} provided the variables \overline{v}_{k} are new to ∃ \overline{x}_{k} (Φ_{1} ∧ … ∧ Φ_{n}).

With this free variable splitting standard (Inner) Skolemization can now be described as: Replace any occurrence of a sub-formula ∃ \overline{x}_{k} (Φ_{1} ∧ … ∧ Φ_{n}) with

Φ_{1}\{x_{i}/f_{i}(\overline{z_{1}}_{l_{1}}, …, \overline{z_{n}}_{l_{n}})\} ∧
Φ_{2}\{x_{i}/f_{i}(\overline{z_{1}}_{l_{1}}, …, \overline{z_{n}}_{l_{n}})\} ∧
⋮
Φ_{n}\{x_{i}/f_{i}(\overline{z_{1}}_{l_{1}}, …, \overline{z_{n}}_{l_{n}})\}

where ⟨\{\overline{z_{1}}_{l_{1}}\}, …, \{\overline{z_{n}}_{l_{n}}\}⟩ is the free variable splitting of ∃ \overline{x}_{k} (Φ_{1} ∧ … ∧ Φ_{n}). The effect of Strong Skolemization now lies in the replacement of some of these variable occurrences with fresh universally quantified variables. The following definition specifies this.

Definition 3.2 (strong skolemization) Let Δ be a first-order sentence in negation normal form. Strong Skolemization replaces existentially quantified sub-formulas of the form ∃ \overline{x}_{k} (Φ_{1} ∧ … ∧ Φ_{n}) with

∀ \overline{w_{2}}_{l_{2}}, \overline{w_{3}}_{l_{3}}, …, \overline{w_{n}}_{l_{n}} Φ_{1}\{x_{i}/f_{i}(\overline{z_{1}}_{l_{1}}, \overline{w_{2}}_{l_{2}}, …, \overline{w_{n}}_{l_{n}})\} ∧
∀ \overline{w_{3}}_{l_{3}}, …, \overline{w_{n}}_{l_{n}} Φ_{2}\{x_{i}/f_{i}(\overline{z_{1}}_{l_{1}}, \overline{z_{2}}_{l_{2}}, \overline{w_{3}}_{l_{3}}, …, \overline{w_{n}}_{l_{n}})\} ∧
⋮
∀ \overline{w_{n}}_{l_{n}} Φ_{n−1}\{x_{i}/f_{i}(\overline{z_{1}}_{l_{1}}, \overline{z_{2}}_{l_{2}}, …, \overline{z_{n−1}}_{l_{n−1}}, \overline{w_{n}}_{l_{n}})\} ∧
Φ_{n}\{x_{i}/f_{i}(\overline{z_{1}}_{l_{1}}, \overline{z_{2}}_{l_{2}}, …, \overline{z_{n}}_{l_{n}})\}

where ⟨\{\overline{z_{1}}_{l_{1}}\}, …, \{\overline{z_{n}}_{l_{n}}\}⟩ is the free variable splitting of ∃ \overline{x}_{k} (Φ_{1} ∧ … ∧ Φ_{n}) and the f_{i}, 1 ≤ i ≤ k are new (Skolem) function symbols.

Note that, in the worst case, each l_{2}, …, l_{n} equals 0, so that Strong Skolemization degenerates to standard Inner Skolemization.

Coming back to the example where we skolemized the sub-formula ∃x (P (x)∧ Q(x, y)) we see that ⟨{}, {y}⟩ is the corresponding free variable splitting, that n = 2, l_{1} = 0, l_{2} = 1, \overline{x_{2}}_{l_{2}} = y, and k = 1, and thus the Strong Skolemization results in (with \overline{w_{2}}_{1} = w) ∀w P (f(w)) ∧ Q(f(y), y).

Let us now come to the proof that Strong Skolemization behaves as desired, i.e., that it preserves both satisfiability and unsatisfiability. To this end we make use of some preliminary definitions as well as an important key lemma.

Definition 3.3 (selector functions, projections) We call any total function h : D^{k} → D^{k} a selector function for a set S ⊆ D^{k} if codomain(h) = S provided S ≠ ∅. In case S = ∅, h may be arbitrary. As usual, the projection functions π_{i} allow us to refer to the ith element of a given sequence, i.e., π_{i}(e_{1}, …, e_{i}, …, e_{n}) = e_{i}.

Such selector functions evidently do exist. For example just take

h(\overline{x}_{k}) = \{ \begin{matrix}\overline{x}_{k} & if \overline{x}_{k} ∈ S \\ \overline{a}_{k} & for some arbitrary \overline{a}_{k} ∈ S if \overline{x}_{k} ∉ S and S ≠ ∅ \\ \overline{b}_{k} & for some arbitrary \overline{b}_{k} ∈ D^{k} if S = ∅ \end{matrix}

Lemma 3.4 If M ⊧ ∃ \overline{x}_{k} (Φ∧Ψ) then M′ ⊧ ∀ \overline{w}_{k} Φ\{x_{i}/h_{i}(\overline{y}_{n}, \overline{w}_{k})\}∧∃ \overline{v}_{k} Ψ\{x_{i}/h_{i}(\overline{y}_{n}, \overline{v}_{k})\}, where \{\overline{y}_{n}\} = V(Φ) \ \{\overline{x}_{k}\} and M′ extends M only by a suitable interpretation of the new function symbols h_{1}, …, h_{k}.

Proof: Let M = (D, ℑ, ϕ) and define

S^{Φ}(\overline{β}_{n}) = \{\overline{α}_{k} | (D, ℑ, [\overline{y}_{n}/\overline{β}_{n}, \overline{x}_{k}/\overline{α}_{k}]) ⊧ Φ\}

Since M ⊧ ∃ \overline{x}_{k} (Φ ∧ Ψ), we know that S^{Φ}(ϕ(\overline{y}_{n})) ≠ ∅, where ϕ(\overline{y}_{n}) is short for the sequence ϕ(y_{1}), …, ϕ(y_{n}). Thus we know that

M[\overline{x}_{k}/\overline{α}_{k}] ⊧ Φ for all \overline{α}_{k} ∈ S^{Φ}(ϕ(\overline{y}_{n})) and
M[\overline{x}_{k}/\overline{α}_{k}] ⊧ Ψ for some \overline{α}_{k} ∈ S^{Φ}(ϕ(\overline{y}_{n}))

Now, for arbitrary \overline{γ}_{n} ∈ D^{n}, let h^{Φ}(\overline{γ}_{n}): D^{k} → D^{k} be a selector function for S^{Φ}(\overline{γ}_{n}) ⊆ D^{k}. Then

M[\overline{x}_{k}/h^{Φ}(ϕ(\overline{y}_{n}))(\overline{α}_{k})] ⊧ Φ for all \overline{α}_{k} ∈ D^{k} and
M[\overline{x}_{k}/h^{Φ}(ϕ(\overline{y}_{n}))(\overline{α}_{k})] ⊧ Ψ for some \overline{α}_{k} ∈ D^{k}

h^{Φ}(ϕ(\overline{y}_{n})) returns sequences of domain elements. Thus, in order to represent a substitute for each of the x_{i}, we have to refer to the respective projections on these sequences, i.e.

M[…, x_{i}/π_{i}(h^{Φ}(ϕ(\overline{y}_{n}))(\overline{α}_{k})), …] ⊧ Φ for all \overline{α}_{k} ∈ D^{k} and
M[…, x_{i}/π_{i}(h^{Φ}(ϕ(\overline{y}_{n}))(\overline{α}_{k})), …] ⊧ Ψ for some \overline{α}_{k} ∈ D^{k}

This immediately leads to a suitable interpretation for the new function symbols h_{1}, …, h_{k} which extend M to M′ by

M′(h_{i})(\overline{β}_{n}, \overline{α}_{k}) = π_{i}(h^{Φ}(\overline{β}_{n})(\overline{α}_{k}))

With this we get

M′[\overline{w}_{k}/\overline{α}_{k}] ⊧ Φ\{x_{i}/h_{i}(\overline{y}_{n}, \overline{w}_{k})\} for all \overline{α}_{k} ∈ D^{k} and
M′[\overline{v}_{k}/\overline{α}_{k}] ⊧ Ψ\{x_{i}/h_{i}(\overline{y}_{n}, \overline{v}_{k})\} for some \overline{α}_{k} ∈ D^{k}

which finally can be simplified to

M′ ⊧ ∀ \overline{w}_{k} Φ\{x_{i}/h_{i}(\overline{y}_{n}, \overline{w}_{k})\} ∧ ∃ \overline{v}_{k} Ψ\{x_{i}/h_{i}(\overline{y}_{n}, \overline{v}_{k})\}

and this completes the proof. □

Theorem 3.5 Strong Skolemization preserves both satisfiability and unsatisfiability. Proof: Unsatisfiability preservation follows immediately from the fact that Strong Skolemization generalizes standard Skolemization. For the other direction assume that

M ⊧ Δ[∃ \overline{x}_{k} (Φ_{1} ∧ … ∧ Φ_{n})]

where Δ is a formula in negation normal form. We prove by induction on the structure of Δ that there exists an interpretation M′ that differs from M only in a suitable interpretation for the new Skolem function symbols f_{1}, …, f_{k} and that satisfies the Strong Skolemization result on the indicated sub-formula. The base case (where Δ = ∃ \overline{x}_{k} (Φ_{1} ∧ … ∧ Φ_{n})) is in fact the crucial part of the proof and requires another induction; this time on the number n. For the case n = 1 Strong Skolemization does not differ from standard Inner Skolemization and we are done. For the induction step assume that M ⊧ ∃ \overline{x}_{k} (Φ_{1} ∧ … ∧ Φ_{n}). Then, by Lemma 3.4, we know that there exists an interpretation M′ such that

M′ ⊧ ∀ \overline{w}_{k} Φ_{1}\{x_{i}/h_{i}(\overline{z_{1}}_{l_{1}}, \overline{w}_{k})\} ∧ ∃ \overline{v}_{k} (Φ_{2} ∧ … ∧ Φ_{n})\{x_{i}/h_{i}(\overline{z_{1}}_{l_{1}}, \overline{v}_{k})\}

where M′ is like M except for the additional interpretation for the new function symbols h_{i}. Now, in order to apply the induction hypothesis on ∃ \overline{v}_{k} (Φ_{2} ∧ … ∧ Φ_{n})\{x_{i}/h_{i}(\overline{z_{1}}_{l_{1}}, \overline{v}_{k})\} recall that the corresponding free variable splitting is given by ⟨\{\overline{z_{1}}_{l_{1}}, \overline{z_{2}}_{l_{2}}\}, \{\overline{z_{3}}_{l_{3}}\}, …, \{\overline{z_{n}}_{l_{n}}\}⟩. Thus, an application of Strong Skolemization leads to the satisfiability of

∀ \overline{w}_{k} Φ_{1}\{x_{i}/h_{i}(\overline{z_{1}}_{l_{1}}, \overline{w}_{k})\} ∧
∀ \overline{w_{3}}_{l_{3}}, …, \overline{w_{n}}_{l_{n}} Φ_{2}\{x_{i}/h_{i}(\overline{z_{1}}_{l_{1}}, \overline{v}_{k})\}\{v_{j}/g_{j}(\overline{z_{1}}_{l_{1}}, \overline{z_{2}}_{l_{2}}, \overline{w_{3}}_{l_{3}}, …, \overline{w_{n}}_{l_{n}})\} ∧
∀ \overline{w_{4}}_{l_{4}}, …, \overline{w_{n}}_{l_{n}} Φ_{3}\{x_{i}/h_{i}(\overline{z_{1}}_{l_{1}}, \overline{v}_{k})\}\{v_{j}/g_{j}(\overline{z_{1}}_{l_{1}}, …, \overline{z_{3}}_{l_{3}}, \overline{w_{4}}_{l_{4}}, …, \overline{w_{n}}_{l_{n}})\} ∧

⋮

∀ \overline{w_{n}}_{l_{n}} Φ_{n−1}\{x_{i}/h_{i}(\overline{z_{1}}_{l_{1}}, \overline{v}_{k})\}\{v_{j}/g_{j}(\overline{z_{1}}_{l_{1}}, …, \overline{z_{n−1}}_{l_{n−1}}, \overline{w_{n}}_{l_{n}})\} ∧
Φ_{n}\{x_{i}/h_{i}(\overline{z_{1}}_{l_{1}}, \overline{v}_{k})\}\{v_{j}/g_{j}(\overline{z_{1}}_{l_{1}}, \overline{z_{2}}_{l_{2}}, …, \overline{z_{n}}_{l_{n}})\}

Instantiating the variables w_{i} in the first conjunct with g_{i}(\overline{z_{1}}_{l_{1}}, \overline{u_{2}}_{l_{2}}, …, \overline{u_{n}}_{l_{n}}) – where the elements in each \overline{u_{j}}_{l_{j}} are fresh universally quantified variables – then reveals the satisfiability of

∀ \overline{u_{2}}_{l_{2}}, …, \overline{u_{n}}_{l_{n}} Φ_{1}\{x_{i}/h_{i}(\overline{z_{1}}_{l_{1}}, \overline{v}_{k})\}\{v_{j}/g_{j}(\overline{z_{1}}_{l_{1}}, \overline{u_{2}}_{l_{2}}, …, \overline{u_{n}}_{l_{n}})\} ∧
∀ \overline{w_{3}}_{l_{3}}, …, \overline{w_{n}}_{l_{n}} Φ_{2}\{x_{i}/h_{i}(\overline{z_{1}}_{l_{1}}, \overline{v}_{k})\}\{v_{j}/g_{j}(\overline{z_{1}}_{l_{1}}, \overline{z_{2}}_{l_{2}}, \overline{w_{3}}_{l_{3}}, …, \overline{w_{n}}_{l_{n}})\} ∧
⋮
∀ \overline{w_{n}}_{l_{n}} Φ_{n−1}\{x_{i}/h_{i}(\overline{z_{1}}_{l_{1}}, \overline{v}_{k})\}\{v_{j}/g_{j}(\overline{z_{1}}_{l_{1}}, …, \overline{z_{n−1}}_{l_{n−1}}, \overline{w_{n}}_{l_{n}})\} ∧
Φ_{n}\{x_{i}/h_{i}(\overline{z_{1}}_{l_{1}}, \overline{v}_{k})\}\{v_{j}/g_{j}(\overline{z_{1}}_{l_{1}}, \overline{z_{2}}_{l_{2}}, …, \overline{z_{n}}_{l_{n}})\}

Now let f_{i}(\overline{u_{1}}_{l_{1}}, …, \overline{u_{n}}_{l_{n}}) = h_{i}(\overline{u_{1}}_{l_{1}}, g_{1}(\overline{u_{1}}_{l_{1}}, …, \overline{u_{n}}_{l_{n}}), …, g_{k}(\overline{u_{1}}_{l_{1}}, …, \overline{u_{n}}_{l_{n}})) for arbitrary \overline{u_{1}}_{l_{1}}, …, \overline{u_{n}}_{l_{n}}. This then leads to the satisfiability of

∀ \overline{w_{2}}_{l_{2}}, \overline{w_{3}}_{l_{3}}, …, \overline{w_{n}}_{l_{n}} Φ_{1}\{x_{i}/f_{i}(\overline{z_{1}}_{l_{1}}, \overline{w_{2}}_{l_{2}}, …, \overline{w_{n}}_{l_{n}})\} ∧
∀ \overline{w_{3}}_{l_{3}}, …, \overline{w_{n}}_{l_{n}} Φ_{2}\{x_{i}/f_{i}(\overline{z_{1}}_{l_{1}}, \overline{z_{2}}_{l_{2}}, \overline{w_{3}}_{l_{3}}, …, \overline{w_{n}}_{l_{n}})\} ∧
⋮
∀ \overline{w_{n}}_{l_{n}} Φ_{n−1}\{x_{i}/f_{i}(\overline{z_{1}}_{l_{1}}, …, \overline{z_{n−1}}_{l_{n−1}}, \overline{w_{n}}_{l_{n}})\} ∧
Φ_{n}\{x_{i}/f_{i}(\overline{z_{1}}_{l_{1}}, \overline{z_{2}}_{l_{2}}, …, \overline{z_{n}}_{l_{n}})\}

and we are done with the base case of the outer induction proof. For the induction step let us assume that Δ = Δ_{1} ∧ Δ_{2}[∃ \overline{x}_{k} (Φ_{1} ∧ … ∧ Φ_{n})]. Then M ⊧ Δ_{1} and M ⊧ Δ_{2}[∃ \overline{x}_{k} (Φ_{1} ∧ … ∧ Φ_{n})]. By the induction hypothesis this means that M ⊧ Δ_{1} and there exists an M′ which extends M only by a suitable interpretation for the function symbols f_{i} and which satisfies the Strong Skolemization result. Since in Δ_{1} there is no mention at all of these function symbols f_{i} we also know that M′ ⊧ Δ_{1} and thus M′ is a model for the altered Δ as well. The cases where Δ is a disjunction, an existential or a universal quantification work analogously so that the respective proofs can be omitted. Note that Δ cannot be of the form ¬Δ_{1}[∃ \overline{x}_{k} (Φ_{1} ∧ … ∧ Φ_{n})] for otherwise it would not be in negation normal form. □

4 Observations and Examples

Strong Skolemization can always be applied whenever standard Skolemization can. However, it does not necessarily produce a different result. For example, in the trivial case n = 1 Strong Skolemization evidently degenerates to Inner Skolemization. Also, if V(Φ_{1}) = V(Φ_{2}) = ⋯ = V(Φ_{n}) it is evident that the corresponding variable splitting is just of the form ⟨\{\overline{x}\}, ∅, …, ∅⟩ and therefore again there is no difference to the corresponding Inner Skolemization result. As a matter of fact, it turns out that the order in which the Φ_{1}, …, Φ_{n} occur plays a crucial rôle for the final Strong Skolemization outcome. In order to obtain an optimal result it ought to be ensured that for no i < j: V(Φ_{i}) ⊃ V(Φ_{j}). If necessary, the Φ_{i} should be rearranged accordingly. In the best case (viewed from the Strong Skolemization perspective) it is possible to rearrange the Φ_{i} in a way such that V(Φ_{1}) ⊂ V(Φ_{2}) ⊂ ⋯ ⊂ V(Φ_{n}) for then each of the l_{j} (see Definition 3.2) is different from 0 and so a maximal number of variable abstractions takes place. The little example we examined in the last section was just of this kind. This leads to the first important observation:

Observation 4.1 Given ∃ \overline{x}_{k} (Φ_{1} ∧ … ∧ Φ_{n}), if at all possible, it should be tried to rearrange the inner conjunctions as ∃ \overline{x}_{k} (Φ_{i_{1}} ∧ … ∧ Φ_{i_{n}}) such that V(Φ_{i_{1}}) ⊆ ⋯ ⊆ V(Φ_{i_{n}}).

Example 4.2 Consider the formula

∀x [C(x) ∨ ∀y ∃z (B(x, y, z) ∧ A(y, z))]  (1)

Since V(B(x, y, z)) ⊃ V(A(y, z)) we should exchange the two conjuncts and therefore consider the formula ∀x [C(x) ∨ ∀y ∃z (A(y, z) ∧ B(x, y, z))] instead. The corresponding free variable splitting then is ⟨{y}, {x}⟩ and thus the Strong Skolemization results in ∀x [C(x) ∨ ∀y (∀w (A(y, f(y, w)) ∧ B(x, y, f(y, x))))] and thus eventually to the clause set

\begin{matrix}C(x) ∨ A(y, f(y, w)) \\ C(x) ∨ B(x, y, f(y, x)) \end{matrix}

Note that an immediate Strong Skolemization step on (1) produces the same result as Inner Skolemization because then the free variable splitting is ⟨{x, y}, ∅⟩.

Such a suitable ordering of the conjuncts cannot always be achieved as shown in the following.

Example 4.3 Consider the formula

∀x [C(x) ∨ ∀y ∃z (A(y, z) ∧ B(x, z))]  (2)

Unfortunately, we cannot follow the above recommendation because there is no subsort relation between the free variables of the two conjuncts. Let us therefore consider both possibilities. Then the free variable splitting we are faced with is either ⟨{y}, {x}⟩, or ⟨{x}, {y}⟩. Now, in order to find out whether one is still to be preferred over the other let us have a look at the two (Strong) Skolemization results. In the first case we get (in clause form)

\begin{matrix}C(x) ∨ A(y, f(w, y)) \\ C(x) ∨ B(x, f(x, y)) \end{matrix}

whereas in the second case we obtain

\begin{matrix}C(x) ∨ B(x, f(x, w)) \\ C(x) ∨ A(y, f(x, y)) \end{matrix}

We can immediately see that for the second case we merely achieved a variant of the standard Skolemization outcome. For the first case, however, a real generalization takes place. A little remark: the first case clauses would have been obtained from standard Skolemization applied to the formula ∀x, y ∃z ((∀u C(u) ∨ A(y, z)) ∧ (C(x) ∨ B(x, z))). The reader may check by her/himself that this is indeed logically equivalent to formula (2).

The above example shows that the “correct” order of the conjuncts can make a difference even if the conjuncts cannot be ordered by way of comparing their respective free variables. Hence, we can suppose that there are a further criteria which might help us to find a more complete ordering of the conjuncts. Notice that in the above example the A-literal has no mention of the variable x and the B-literal has no mention of the variable y and that Δ^{y} is a sub-formula of Δ^{x}. This is no coincidence. The conjunct A(y, z) should be considered first because the quantifier of the variable y is “closer” to A(y, z) than the quantifier of the variable x to B(x, z). There is thus a better chance that the other literals that possibly occur in the final clausification result in the same clause have no mention of y at all and so the possibility increases that some clauses consist of variable-disjoint sub-clauses.

Observation 4.4 Let Δ be a closed formula in negation normal form (with all universal quantifications moved inwards as far as possible)^{6}, and let ∃ \overline{x}_{k} (Φ_{1} ∧ … ∧ Φ_{n}) be a sub-formula of Δ (for simplicity let us assume that this sub-formula lies not within the scope of another existential quantifier). In case V(Φ_{i}) and V(Φ_{j}) are incomparable for some i, j then consider Φ_{i} first provided there exists a v ∈ V(Φ_{j}) such that for all w ∈ V(Φ_{i}): Δ^{w} is a sub-formula of Δ^{v}.

Evidently, the observations from above do not provide us with a total ordering on sub-formulas. Such a total ordering is in fact not possible as the following example illustrates.

Example 4.5 Consider the formula

∀x, y [C(x, y) ∨ ∃z (A(y, z) ∧ B(x, z))]  (3)

Unfortunately it is not possible to follow the recommendation of Observation 4.4 because there is no “nearer” quantification. We therefore obtain either

\begin{matrix}C(x, y) ∨ A(y, f(w, y)) \\ C(x, y) ∨ B(x, f(x, y)) \end{matrix}

or, alternatively,

\begin{matrix}C(x, y) ∨ B(x, f(x, w)) \\ C(x, y) ∨ A(y, f(x, y)) \end{matrix}

6This restriction is not necessary; however, it may help as Example 4.3 shows.

There is no way to decide which might be more valuable. This depends on the other clauses of the whole problem under consideration and not on this formula alone. For instance, if the rest of the problem implies that ∀y ¬C(t, y) for some term t then the first possibility should be preferred. If, however, the rest of the problem implies ∀x ¬C(x, t) for some term t then the second possibility seems more valuable. But note: we cannot choose a “wrong” one; both are more general than the corresponding standard Skolemization result.

The above example is not artificial. As an interesting instance consider the so-called “density property” of some binary relation R, i.e.,

∀x, y [R(x, y) ⊃ ∃z (R(x, z) ∧ R(z, y))]  (4)

Here, as in the previous example, Strong Skolemization ends up with either

\begin{matrix}¬R(x, y) ∨ R(x, f(x, w)) \\ ¬R(x, y) ∨ R(f(x, y), y) \end{matrix} or \begin{matrix}¬R(x, y) ∨ R(x, g(x, y)) \\ ¬R(x, y) ∨ R(g(w, y), y) \end{matrix}

The former is particularly interesting if R can be proven to be forward serial, whereas the latter is more important in case backward seriality of R holds. Note that the results achieved from Strong Skolemization are identical to the application of standard Skolemization on

∀x, y ∃z [∀w (R(x, w) ⊃ R(x, z)) ∧ (R(x, y) ⊃ R(z, y))]  (5)

and

∀x, y ∃z [(R(x, y) ⊃ R(x, z)) ∧ ∀w (R(w, y) ⊃ R(z, y))]  (6)

respectively. I leave it to the reader to verify that (4), (5), and (6) are pairwise equivalent.

The above examples show that the Strong Skolemization outcome can depend on the choice of the conjunct. Quite often, however, this choice turns out to be irrelevant because the possible cases are somewhat symmetric. One such example can be found in the following.

Example 4.6 Consider the formula

∀x, y, z [(R(x, y) ∧ R(x, z)) ⊃ ∃u (R(y, u) ∧ R(z, u))]  (7)

which expresses something like a “confluence” property of the relation R. Standard Skolemization (plus clausification) results in

\begin{matrix}¬R(x, y) ∨ ¬R(x, z) ∨ R(y, f(y, z)) \\ ¬R(x, y) ∨ ¬R(x, z) ∨ R(z, f(y, z)) \end{matrix}

whereas Strong Skolemization yields

\begin{matrix}¬R(x, y) ∨ ¬R(x, z) ∨ R(y, f(y, w)) \\ ¬R(x, y) ∨ ¬R(x, z) ∨ R(z, f(y, z)) \end{matrix}

Here, condensing is possible on the literals ¬R(x, y) and ¬R(x, z) with substitution σ = {z/y} and so we end up with

\begin{matrix}¬R(x, y) ∨ R(y, f(y, w)) \\ ¬R(x, y) ∨ ¬R(x, z) ∨ R(z, f(y, z)) \end{matrix}

Similarly, if we exchange the two conjuncts, Strong Skolemization leads to (again after condensing)

\begin{matrix}¬R(x, y) ∨ ¬R(x, z) ∨ R(y, g(y, z)) \\ ¬R(x, z) ∨ R(z, g(w, z)) \end{matrix}

In contrast to the earlier examples the two outcomes are mere variants of each other. Nevertheless, both subsume the standard Skolemization result.

The above examples are all of the form ∃x (Φ∧Ψ). However, the definition of Strong Skolemization also covers the more general cases in which there is more than just one existentially quantified variable and more than just two conjuncts. Such more general cases usually cannot be simulated by a sequence of Strong Skolemization steps of the above kind. It is even the case that it is sometimes preferable to avoid anti-prenexing as the following example shows.

Example 4.7 Let

Δ = ∀x [A(x) ∨ ∃u, v (B(u) ∧ C(u, v) ∧ D(x, u, v))]  (8)

Standard Skolemization then results in

∀x [A(x) ∨ (B(f(x)) ∧ C(f(x), g(x)) ∧ D(x, f(x), g(x)))]

whereas Strong Skolemization leads to

∀x [A(x) ∨ (∀w B(f(w)) ∧ ∀w C(f(w), g(w)) ∧ D(x, f(x), g(x)))]

If we first performed an anti-prenexing on the input formula, however, we would have to deal with

∀x [A(x) ∨ ∃u (B(u) ∧ ∃v (C(u, v) ∧ D(x, u, v)))]

and thus obtained by Strong Skolemization

∀x [A(x) ∨ (∀w B(f(w)) ∧ C(f(x), g(x)) ∧ D(x, f(x), g(x)))]

which, although being more general than the standard Skolemization result, is less general than what we would obtain when we did without an initial antiprenexing.

Observation 4.8 Anti-prenex transformations cannot absolutely be recommend. Rather, existential quantifiers should be moved outwards over conjunctions in order to obtain more general results.

In the worst case Strong Skolemization behaves like standard Inner Skolemization. There are, however, sub-languages of first-order predicate logic for which Strong Skolemization is necessarily superior to standard Skolemization techniques. For instance, in the translation of modal or terminological logic formulas (like ALC; see the paper by Schmidt-Schauß and Smolka (1991)) we have to deal with certain syntactic restrictions in the translation result which fit perfectly well to Strong Skolemization. I do not want to go into detail what these languages is concerned. What is important for our purpose, however, is that after performing a so-called relational translation into first-order predicate logic we are faced with formulas that contain sub-formulas of the kind ∃x [R(y, x) ∧ Φ[x]] where R is a binary predicate symbol and Φ[x] is a representative of a more or less complicated formula with x as its only free variable. Here Strong Skolemization nicely comes into play. Why this is so is justified by the following observation.

Observation 4.9 Let Δ be a sentence with sub-formula ∃x (Φ ∧ Ψ) such that x is the only free variable in Φ and let {y_{1}, …, y_{n}} = V(Ψ) \ {x}. Then Strong Skolemization transforms Δ[∃x (Φ ∧ Ψ)] into

Δ[∃x (Φ ∧ Ψ) / ∀ \overline{w}_{n} Φ\{x/f(\overline{w}_{n})\} ∧ Ψ\{x/f(\overline{y}_{n})\}]

where f is a new n−place function symbol. Note that the sub-formula ∀ \overline{w}_{n} Φ\{x/f(\overline{w}_{n})\} obtained this way has no free variables at all. This is of particular importance after clause normal form generation takes place, for it allows us to split clauses into variable disjoint sub-clauses and thus splits the reasoning process into several independent branches.

In running a huge ALC database we have found that in about half of the examples there was a significantly better performance after Strong Skolemization than after standard Inner Skolemization. In approximately one fourth of all examples Strong Skolemization made it at all possible for the theorem prover to stop its reasoning process, be it with a proof or with a saturated set of clauses.^{7}

Such gains have been proved true by testing other collections of first-order theorems as, e.g., in (Pelletier 1986). For instance, the first-order presentation of the (in)famous “Pigeon-Hole Problems” allows only for one single application of Strong Skolemization, namely at the sub-formula

∀x Object(x) → ∃y (Hole(y) ∧ In(x, y))

Standard Skolemization leads to ∀x Object(x) → (Hole(f(x)) ∧ In(x, f(x))) whereas Strong Skolemization yields the more general

∀x Object(x) → (∀w Hole(f(w)) ∧ In(x, f(x)))

7Evidently, there are specially designed inference mechanisms and translation techniques whose performance is even better. It is certainly not our aim to compete with these methods; our aim was just to illustrate the superiority of Strong Skolemization over standard Skolemization.

Depending on the theorem prover at hand this generalization gives rise to a time gain of 10-40%.

Summarizing: Standard Inner Skolemization and Strong Skolemization can best be compared by having a closer look at the respective final clausification results. It turns out that the structure of the clauses is preserved; also the number of clauses and the number of literals within clauses remains as in the standard case. The difference lies in the abstraction from some of the variables in Skolem functions resulting in new universally quantified variables. This abstraction can help to simplify and/or to split clauses without jeopardizing soundness and completeness of the underlying calculus. And, moreover, its costs are essentially the costs of standard Skolemization; there is no high price to be paid for the gain.

5 Related Work

There is a somewhat related technique to Strong Skolemization, the so-called Optimized Skolemization, that has been developed by Christoph Weidenbach and Hans Jürgen Ohlbach in (1995). Slightly generalizing, their approach can briefly be described as follows:

Definition 5.1 ((generalized) optimized skolemization) Let Δ[∃ \overline{x}_{k} (Φ ∧ Ψ)] be a sentence in negation normal form and let us assume that Δ ⊧ ∀ \overline{y}_{n} ∃ \overline{x}_{k} Φ where \{y_{1}, …, y_{n}\} = V(∃ \overline{x}_{k} (Φ ∧ Ψ)). Then

Δ is satisfiable iff ∀ \overline{y}_{n} Φ\{x_{i}/f_{i}(\overline{y}_{n})\} ∧ Δ[∃ \overline{x}_{k} (Φ ∧ Ψ)/Ψ\{x_{i}/f_{i}(\overline{y}_{n})\}] is satisfiable

where f_{1}, …, f_{k} are new (Skolem) function symbols.

Note that Optimized Skolemization involves a theorem prover on its own to prove the intermediate goal Δ ⊧ ∀ \overline{y}_{n} ∃ \overline{x}_{k} Φ. Since this can be arbitrarily complicated, an implementation of Optimized Skolemization has to somehow restrict the resources for this intermediate theorem prover in order to eventually come to a decision (Weidenbach, Gaede and Rock 1996).

As an example consider again the density property for R, i.e., ∀u, v [R(u, v) ⊃ ∃w (R(u, w) ∧ R(w, v))]. In case we know (or can easily prove) that the binary relation R is serial, i.e., ∀x∃y R(x, y), the Optimized Skolemization of the density property results in the clauses

\begin{matrix}R(x, f(x, y)) \\ ¬R(u, v) ∨ R(f(u, v), v) \end{matrix}

The very same two clauses could be obtained by standard Skolemization from

∀x, y ∃z [R(x, z) ∧ (R(x, y) ⊃ R(z, y))]  (9)

I leave it to the reader to verify that the formula (9) is logically equivalent to the conjunction of seriality and density for R.

Now let us compare this with the method proposed in this paper. Recall that Strong Skolemization finally results in the clauses

\begin{matrix}¬R(u, v) ∨ R(u, f(u, w)) \\ ¬R(u, v) ∨ R(f(u, v), v) \end{matrix}

Moreover, suppose that there is a further clause, say R(x, g(x)), which states the seriality of R. Then a resolution step with the first clause from above yields the unit clause R(u, f(u, w)) which even subsumes its two-literal parent clause. Thus, we finally end up with the same result as the Optimized Skolemization, i.e., Optimized Skolemization has in a sense been simulated by Strong Skolemization and Resolution.

The above shows some similarity between Strong Skolemization and Optimized Skolemization. However, the similarities are not always as strong as the above example might suggest.

Consider again formula (7) and assume that we are able to prove that ∀y∃u R(y, u), i.e., R is serial. Optimized Skolemization then results in the clauses

\begin{matrix}R(y, f(y, z)) \\ ¬R(x, y) ∨ ¬R(x, z) ∨ R(z, f(y, z)) \end{matrix}

whereas Strong Skolemization on R(y, u) leads to

\begin{matrix}¬R(x, y) ∨ R(y, f(y, w)) \\ ¬R(x, y) ∨ ¬R(x, z) ∨ R(z, f(y, z)) \end{matrix}

Note that – in contrast to the “density example” – the seriality of R does not help here to entirely simulate Optimized Skolemization, although, somewhat surprisingly, backward seriality would; and, after all, seriality follows from backward seriality in the example under consideration (although not the other way round). A major reason for this is, that Optimized Skolemization takes the whole problem into account and not only the sub-problem in which the sub-formula to be skolemized occurs. In other words, Optimized Skolemization works globally on the problem under consideration whereas Strong Skolemization applies only locally to the various sub-problems. This might lead to the conclusion that, if Optimized Skolemization applies at all, then it produces a more general result than Strong Skolemization and thus in particular a more general result than standard Skolemization. This, however, is not quite true, for, consider again formula (8)

∀x [A(x) ∨ ∃y, z (B(y) ∧ C(y, z) ∧ D(x, y, z))]

There are three possible entry points for Optimized Skolemizations to start, one for each conjunct. I.e., it is tried to prove from the rest of the problem that either of the following holds: ∃y B(y), ∃y, z C(y, z), or, ∀x∃y, z D(x, y, z). If none can be proved then Optimized Skolemization returns the very same as standard Inner Skolemization. Otherwise it comes up with one the following clause sets

\begin{matrix}B(f(x)) & A(x) ∨ B(f(x)) & A(x) ∨ B(f(x)) \\ A(x) ∨ C(f(x), g(x)) & C(f(x), g(x)) & A(x) ∨ C(f(x), g(x)) \\ A(x) ∨ D(x, f(x), g(x)) & A(x) ∨ D(x, f(x), g(x)) & D(x, f(x), g(x)) \end{matrix}

Now let us compare these with the corresponding Strong Skolemization result, i.e., with the clauses

A(x) ∨ B(f(w))
A(x) ∨ C(f(w), g(w))
A(x) ∨ D(x, f(x), g(x))

The first and the second of the above three clauses can be split into two variable disjoint sub-clauses respectively. This leaves us with two branches of the reasoning process, namely one which contains merely the unit clause A(x) and one which contains the clauses

B(f(x))
C(f(x), g(x))
A(x) ∨ D(x, f(x), g(x))

This clause set subsumes the first two possibilities from Optimized Skolemization. Only for the third possibility we cannot seriously make a prediction: It depends on the rest of the problem under consideration. At least the supposed superiority of Optimized Skolemization compared to Strong Skolemization begins to falter.

Now, one might object that we could apply Optimized Skolemization by checking a more complex conjunct first, namely ∃y, z (A(y) ∧ B(y, z)). After all, if this turns out to be provable from the rest of the problem then Optimized Skolemization would end up in exactly the same branch as Strong Skolemization, and that without having to consider the other branch as well, thus again showing its superiority. Fair enough, but we have to bear in mind that Optimized Skolemization involves theorems to be proven (automatically). And the more intermediate theorems there are, the more effort is to be spent for the clausification procedure alone. Thus, in order to reduce this effort, real implementations of the Optimized Skolemization method (see (Weidenbach et al. 1996)) avoid considering all possible combinations of conjuncts; rather they consider one conjunct after the other and as soon as one attempt turns out to be successful they take this one as the candidate. In the example above, for instance, this means that Optimized Skolemization performs at most three intermediate proofs, whereas in case we checked every combination there were many more such attempts.

Summarizing: In comparing standard Skolemization with Optimized Skolemization on the one hand and Strong Skolemization on the other hand we can see that Optimized Skolemization essentially cuts off literals from clauses of the standard clausification result whereas Strong Skolemization replaces some of the variables by new ones. It is not always clear which of the two is to be preferred, although it seems that in practice Optimized Skolemization comes up with slightly better results. The price to be paid for this, however, is that Optimized Skolemization requires a theorem prover on its own in order to prove its intermediate lemmas. If these proof attempts fail, be it because the goal cannot be proven or the necessary resource limitations on the prover prevent us to find a proof, then Optimized Skolemization performs a standard Inner Skolemization step and therefore shows no advantage at all in such cases. Latest at this stage, if not earlier simply because the implementer of the clause normal form generator is not willing to include a full theorem prover into his/her algorithm, Strong Skolemization can come into play. In fact, it can even be imagined that it would make sense to perform both Optimized and Strong Skolemization and to compare the respective results. Whatever seems more valuable should be chosen, and this could vary from case to case, i.e., from sub-formula to sub-formula.

It might even be possible to combine the two techniques. How this could be done is still an open question and requires some further work.

References

Andrews, P. B.: 1981, Theorem Proving via General Mating, Journal of the Association for Computing Machinery 28(2), 193–214.

Baaz, M. and Leitsch, A.: 1994, On Skolemization and Proof Complexity, Fundamenta Informaticae 20, 353–379.

Chang, C.-L. and Lee, R. C.: 1973, Symbolic Logic and Mechanical Theorem Proving, Computer Science and Applied Mathematics Series, Academic Press, New York.

Egly, U.: 1994, On the Value of Antiprenexing, Proceedings of the LPAR’94, Springer, LNAI 822.

Loveland, D.: 1978, Automated Theorem Proving: A Logical Basis, Fundamental Studies in Computer Science, North-Holland.

Nonnengart, A.: 1996, Strong Skolemization, Technical Report MPI-I-96-2-010, Max-Planck-Institut für Informatik, Saarbrücken, Germany. http://www.mpi-sb.mpg.de/∼nonnenga/publications/.

Ohlbach, H. J. and Weidenbach, C.: 1995, A Note on Assumptions about Skolem Functions, Journal of Automated Reasoning 15(2), 267–275.

Pelletier, F. J.: 1986, Seventy-Five Problems for Testing Automatc Theorem Provers, Journal of Automated Reasoning 2(2), 191–216.

Schmidt-Schauß, M. and Smolka, G.: 1991, Attributive Concept Description with Complements, Artificial Intelligence 48, 1–26.

Skolem, T.: 1920, Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit oder Beweisbarkeit mathematischer Sätze, nebst einem Theoreme über dichte Mengen, Skrifter utgit av Videnskappsellkapet i Kristiania 4, 4– 36. see also: (Skolem 1976).

Skolem, T.: 1976, Logico-combinatorial Investigations in the Satisfiability and Provability of Mathematical Propositions, in J. van Heijenoort (ed.), From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931, Harvard University Press.

Weidenbach, C., Gaede, B. and Rock, G.: 1996, SPASS & FLOTTER Version 0.42, Proceedings of the 13th International Conference on Automated Deduction, CADE 13, Springer, LNAI 1104, pp. 141–145.