Quantifier Elimination

in

Second-Order Predicate Logic

Diplomarbeit Thorsten Engel

Saarbrücken, 1996 Author’s Address

Thorsten Engel Max-Planck-Institut für Informatik Im Stadtwald 66123 Saarbrücken/Germany E-mail: engel@mpi-sb.mpg.de

Advisors:

Prof. Hans Jürgen Ohlbach, Imperial College London Prof. Dov Gabbay, Imperial College London

Declaration

Ich erkläre, die vorliegende Arbeit selbständig im Sinne der Diplomprüfungsordnung erstellt und ausschließlich die angegebenen Quellen und Hilfsmittel benutzt zu haben.

Saarbrücken, den 20.10.1996

Thorsten Engel

Acknowledgments

Thanks to Hans-Jürgen, for his part of the patience this work demanded from both of us, and his belief that something would come out of it. Thanks to Renate and Ullrich, who always had an open ear and a free halfan-hour for my just-a-second questions. Thanks to Volker, for continuous supply with luxury goods, such as moral support and Darjeeling tea, and last-minute help. Thanks to Kai, Maren and Hannah, to Hannah with a twinkle, for their help with this work, and anyway. Finally, thanks to Frigga Engel and Horst Engel, for the least scientific and most natural contribution to this work, and for some support.

Contents

1 Introduction 5 1.1 Reduction of second-order formulas . . . . . . . . . . . . . . . 6 1.2 Elimination of existentially quantified predicate symbols … 7 1.3 Elimination of existentially quantified function symbols … 7 1.4 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

2 Notation 10 2.1 First- and second-order logic . . . . . . . . . . . . . . . . . . 10 2.2 Miscellaneous . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

3 General complexity of second-order quantifier elimination 13 3.1 Expressiveness of second-order logic . . . . . . . . . . . . . . 13 3.2 Characterizing first-order logic . . . . . . . . . . . . . . . . . 15 3.3 Computational complexity of reduction . . . . . . . . . . . . 16 3.4 Reducible fragments of second-order logic . . . . . . . . . . . 24

4 Scan: Elimination of existentially quantified predicates 26 4.1 The basic Scan algorithm . . . . . . . . . . . . . . . . . . . . 26 4.2 Extensions of the basic algorithm . . . . . . . . . . . . . . . . 34

5 Unskolemize: Elimination of existentially quantified functions 48 5.1 The problem of skolem functions in Scan . . . . . . . . . . . 48 5.2 Reversing skolemization as function elimination . . . . . . . . 49 5.3 Extensions of Unskolemize . . . . . . . . . . . . . . . . . . . 66 5.4 The McCune algorithm . . . . . . . . . . . . . . . . . . . . . 68 5.5 Some remarks on the scope and complexity of Unskolemize 69 5.6 Future work . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71 6 Implementation of Scan and Unskolemize 73

6.1 The roots: Otter . . . . . . . . . . . . . . . . . . . . . . . . 73 6.2 Scan features and how to use them . . . . . . . . . . . . . . . 74 6.3 Implementation of Scan . . . . . . . . . . . . . . . . . . . . . 74 6.4 The user interface . . . . . . . . . . . . . . . . . . . . . . . . 80 6.5 Details of the implementation . . . . . . . . . . . . . . . . . . 89 6.6 Modules and source files . . . . . . . . . . . . . . . . . . . . . 94 6.7 Installation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95

A Syntax of formulas and clauses in Scan 97 A.1 Names for Variables, Constants, Functions, and Predicates . . 97 A.2 Terms and Atoms . . . . . . . . . . . . . . . . . . . . . . . . . 98 A.3 Literals and Clauses . . . . . . . . . . . . . . . . . . . . . . . 99 A.4 Formulas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99 A.5 Infix, Prefix, and Postfix Expressions . . . . . . . . . . . . . . 101 A.6 Whitespace in Expressions . . . . . . . . . . . . . . . . . . . . 103 A.7 Bugs, etc., in Input and Output of Expressions . . . . . . . . 104 A.8 Examples of Operator Declarations . . . . . . . . . . . . . . . 104

List of Figures 107

Chapter 1

Introduction

Mathematical logic is concerned with formalizing mathematical notions and reasoning about them. For this purpose, classical predicate logic has been developed. Now there is an ongoing dispute with a long tradition about the type of quantifiers a logic must provide to be able to express certain notions. Is first-order logic sufficient, or not even second-order logic?

Whatever the choice, there is a fatal trade-off between the expressive power of a logic and the complexity of deduction within this logic: For example, first-order logic is complete, but fails in characterizing, for example, the class of finite models. In second-order logic, on the other hand, this class can be characterized, and this can be done with a simple second-order expression (see chapter 3 for this example in depth). Likewise, many natural formulations of mathematical problems have a second-order form. However, there can be no complete deduction system for second-order logic, which has already been shown by Gödel ([Göd30], for a modern exposition see van Benthem and Doets [vBD84]).

In this situation, we might try to computationally decide whether a problem, formulated as a set of second-order formulas, also has a first-order formulation, and compute a first-order translation if it exists. We could then first describe a problem in a second-order language, translate it into firstorder logic and then reason about it in a complete system for first-order logic. Furthermore, for certain problems arising for example in correspondence theory ([vB84]), sometimes the translation itself is the solution of a problem.

Of course, we would not seriously expect that there is any sound and complete algorithm able to make this decision for full second-order logic, and van Benthem and Doets show that these expectations can be proven correct ([vBD84]). Still, for subclasses of second-order logic essentially more expressive than first-order logic, powerful reduction algorithms have been developed.

1.1 Reduction of second-order formulas

Already Ackermann ([Ack35a], [Ack35b]) has proposed basically two algorithms for transforming certain second-order formulas into equivalent firstorder formulas. One of his methods works by transforming formulas into a form that can be easily reduced. It is explained in detail and extended by Szalas in [Sza92]. The other method can be seen as a special case of a recent approach by Gabbay and Ohlbach ([GO92]). Both methods try to compute a set of first-order consequences of a second-order formula that is equivalent to this formula and free of redundancies. The formulation by Gabbay and Ohlbach is simpler and more direct than the one of Ackermann. Yet another approach by Nonnengart and Szalas [NS95] computes fixpoints of formula series to find reductions.

However, these algorithms only eliminate predicate quantifiers in secondorder formulas. They work on normalized formulas containing skolem functions, and their output may also contain skolem functions. In this context, skolem functions must be interpreted as existentially quantified functions, so formulas containing them are still second-order formulas. None of the algorithms can be used in an obvious way to eliminate these functions, and only in [GO92] there is a sketch of how to do this. McCune addresses the problem of skolem function elimination in [McC88]. His algorithm eliminates skolem functions by reversing the well-known skolemization process. It only tries to preserve satisfiability of a formula, but can easily be proven to be equivalence preserving. However, it fails to eliminate functions for some formulas that have been obtained by skolemization, and has exponential complexity.

In this work, we present the algorithm Unskolemize for function elimination that is also based on the idea of reversing skolemization. It reduces a larger class of formulas than the McCune algorithm, and solves a subproblem in quadratic time that the McCune algorithm computes in polynomial time in the worst case. Furthermore, we present the Scan algorithm as developed by Gabbay and Ohlbach in [GO92]. We add some optimizations that enlarge the set of formulas for which the algorithm terminates. Besides, we describe a C++-implementation of the two algorithms based on the well-known theorem prover Otter. On the theoretical side, we collect some known fundamental results relating second-order quantifier elimination and some basic observations on its computational aspects.

1.2. ELIMINATION OF EXISTENTIALLY QUANTIFIED PREDICATE SYMBOLS7

We will now shortly sketch the methods employed by the Scan and the Unskolemize algorithm.

1.2 Elimination of existentially quantified predicate symbols

Assume we are given the first-order formula

ϕ =^{def} (P ∨ Q) ∧ (¬P ∨ R)

and now consider the second-order formula

Φ =^{def} ∃P ϕ.

It is clear that any first-order equivalent of Φ must still imply all consequences of Φ. Especially, it must imply all first-order consequences, that is, consequences expressible as a first-order statement. In a naive approach, we try to generate all P -free first-order consequences of ϕ and then check whether they are already equivalent to Φ.

To this end, we only consider the first-order part ψ =^{def} (P ∨Q)∧(¬P ∨R) of ϕ, treat P as a simple first-order predicate and compute the set of firstorder consequences by resolution. We obtain the single resolvent

Res =^{def} Q ∨ R.

It is easily checked that Res ≡ Φ: Φ ⊧ Res holds because of correctness of resolution. For the other direction, given a model M that verifies Res, we have to choose an interpretation for P so that M verifies ϕ with this interpretation. Now if M verifies R, choose P to be true, and if M verifies Q, choose P to be false. Then M also verifies Φ.

Essentially this method of generating resolvents is extended in chapter 4, yielding the Scan algorithm.

1.3 Elimination of existentially quantified function symbols

As is shown in chapter 5, the Scan algorithm for predicate symbol elimination cannot simply be used as an algorithm for function symbol elimination by just coding functions as predicates. A different approach is suggested by the well-known operation of skolemization, which may be seen as an application of a second-order rewrite rule as described in chapter 5.

Let ϕ be the formula ∀x∃yP (x, y). This is typically skolemized to P (x, f_{y}(x)), where f_{y} is a new skolem function. In the context of automated theorem proving, where skolemization is employed, it is shown to be a satisfiability preserving transformation. However, as is explained in chapter 5, with the argument usually employed we could also show the stronger equivalence

∀x∃y P (x, y) ≡ ∃f_{y}∀x P (x, f_{y}(x)).

We can generalize this by taking a formula ϕ(x̄, y) instead of P, which contains y and the vector x̄ as free variables, then

∀x̄∃y ϕ(x̄, y) ≡ ∃f_{y}∀x̄ ϕ(x̄, f_{y}(x̄)).

This rewrite rule can now be used for eliminating existentially quantified function symbols, which we shall call skolem functions, by using it backwards, replacing a second-order quantifier with a first-order quantifier. This is less simple as it seems at first sight, because we usually encounter more than one skolem function, which all have to be unskolemized in parallel.

1.4 Overview

The second chapter introduces necessary notation.

The third chapter assembles some known results that are relevant for automated quantifier elimination and shows their implications for its computational complexity. The quoted theorems involve characterization results for first-order logic. Most of the results concern the sheer computability of different reduction problems, but we also derive a complexity result for the time-complexity of reducing second-order quantified propositional formulas. We also prove by elementary means that there cannot be a complete reduction algorithm on undecidable fragments of second-order logic, a theorem elsewhere proven in more complicated ways or using sophisticated machinery.

In the fourth chapter, we present the Scan algorithm for predicate elimination. A number of optimizations are introduced that improve its performance, its termination properties and the compactness of its output.

The fifth chapter is concerned with the Unskolemize algorithm for function elimination. We show its correctness, sketch a completeness proof for a certain class of formulas and show that it can probably lead to an algorithm with only quadratic time complexity, as opposed to the existing algorithm by McCune, which has polynomial time complexity.

Finally, the sixth chapter describes Scan, the implementation of the algorithms Scan and Unskolemize and how it is founded on the theorem prover Otter. It comprises a quick introduction and a user manual.

Notation

This chapter will gather some basic notions and notational conventions.

2.1 First- and second-order logic

We assume the standard notions such as term, clause, formula etc. of firstorder logic to be known, as presented for example in [HET84]. We use a restricted version of second-order logic, which is the subset of second-order logic consisting of formulas not containing predicates as arguments of other predicates. Quantifiers over predicates range over all predicates over a given domain. With Σ_{1}^{1}, we denote the set of all second-order formulas Φ which have the following form:

Φ = ∃P_{1}, …, P_{n}ϕ

where ϕ is a formula of first-order logic. Analogously, Π_{1}^{1} denotes the set of second-order formulas Φ of the form

Φ = ∀P_{1}, …, P_{n}ϕ.

Models are written as pairs M = ⟨D, I⟩, where D denotes a domain and I an interpretation. Assignments are written as A. We denote the interpretation of a formula ϕ (or a term) by ϕ^{I}, with an additional assignment by ϕ^{I,A}.

We use lower cases x, y or z for variable names, P, Q or R for predicates, and f, g, h for functions. Constants are designated with lower cases of the beginning of the alphabet: a, b, c, . . .. We will designate formulas of firstorder logic with the Greek lower cases θ, ϕ, ψ, χ.

We abbreviate vectors of of quantifiers by writing ∃x̄ϕ for a formula beginning with a prefix of existential quantifiers, i.e., a formula of the form ∃x_{1}r … ∃x_{n}ϕ. Similarly, ∀ȳϕ abbreviates a formula starting with a prefix of universal quantifiers, and ∀∃P̄ϕ a formula with a mixed prefix of both universal and existential quantifiers.

We will need a simple complexity measure on formulas that counts the maximum nesting depth of quantifiers:

Definition 2.1.1 (Quantifier rank of a formula) The quantifier rank qr(ϕ) of a first-order formula ϕ is recursively defined as follows:

• if ϕ is atomic, then qr(ϕ) = 0.

• if ϕ = ¬ψ, then qr(ϕ) = qr(ψ).

• if ϕ = ψ_{1} ∘ ψ_{2}, for a binary connective ∘ ∈ {∧, ∨, ⇒, ⇔}, then qr(ϕ) = max(qr(ψ_{1}), qr(ψ_{2})).

• if ϕ = ∀ψ or ϕ = ∃ψ, then qr(ϕ) = qr(ψ) + 1.

2.2 Miscellaneous

We use substitutions and related notions.

Definition 2.2.1 (Substitution) A substitution is a finite set of variable/ term pairs σ = {x_{1} ↦ t_{1}, x_{2} ↦ t_{2}, …, x_{n} ↦ t_{n}}, where x_{i}σ = t_{i}, 1 ≤ i ≤ n. The domain of a substitution σ is the set Dom(σ) = {x | x ≠ xσ}.

As usual, substitutions are designated with Greek lower cases σ, μ, ν. We write tσ or σ(t) to denote the result of applying the substitution σ to t.

For accessing subterms in terms, we define Occurrences.

Definition 2.2.2 (Occurrences) An occurrence is a word over IN. Let ϵ denote the empty word. We first define the set of occurrences of terms t and variables v, Occ(t) and Occ(v), then the set of occurrences of a formula ϕ.

1. for all variables v ∈ V, Occ(v) = ∅.

2. the empty word ϵ is in Occ(t)

3. i.π is in Occ(t) if t = f(t_{1}, …, t_{n}) and π ∈ Occ(t_{i}).

The set of occurrences of a formula ϕ, Occ(ϕ) is defined as follows:

1. the empty word ϵ is in Occ(ϕ)

2. i.π is in Occ(ϕ) if ϕ is the atomic formula P (t_{1}, …, t_{n}), i ≤ n and π ∈ Occ(t_{i}).

3. i.π is in Occ(ϕ) if ϕ = ψ_{1} ∧ … ∧ ψ_{n} or ϕ = ψ_{1} ∨ … ∨ ψ_{n}, i ≤ n and π ∈ Occ(ψ_{i})

4. 1.π (2.π) is in Occ(ϕ) if ϕ = ∀x ψ or ϕ = ∃x ψ or ϕ = ¬ψ or ϕ = ψ ⇒ θ or ϕ = ψ ⇔ θ and π ∈ Occ(ψ) (π ∈ Occ(θ)).

Given a term, variable or a formula and a position, we can get a term, variable or a subformula at that position: if π ∈ Occ(ψ) then ψ|_{ϵ} = ψ and ψ|_{i.π} = ψ_{i}|_{π} where ψ = ψ_{1} ∘ … ∘ ψ_{n}, ∘ ∈ {∧, ∨, ⇒, ⇔}, and 1 ≤ i ≤ n, or ψ|_{1.π} = ϕ|_{π} if ψ = ¬ϕ or ψ = ∀x ϕ or ψ = ∃x ϕ.

We obtain the set of all occurrences of a term s in a formula ϕ or a term t with Occ(ϕ, s) and Occ(t, s).

We write ϕ[π/ψ] for the formula obtained from ϕ by replacing the formula at the position π by ψ, analogously t[π/s] for terms s, t.

Additionally we define the length of an occurrence π to be the length of the word π over IN.

General complexity of second-order quantifier elimination

Before we step into the details of practical quantifier elimination in the next chapter, it is worth noting some of the most basic theoretical limitations we have to face. One natural source of difficulties is the expressiveness of second-order logic, making it impossible to find a first-order equivalent for every formula of second-order logic in principle. We will exemplify this by the non-first-order notion of finiteness. Some results about the overall expressiveness of second-order logic will further illustrate its distance and relation to first-order logic.

However, as the next chapter will show, it is well possible to design practically usable algorithms for eliminating second-order quantifiers. Some simple observations will relate their termination properties to the decidability of the fragments of second-order logic they are operating on. In particular, it can be proven by elementary means that there is no algorithm computing first-order- equivalents of second order formulas if they exists and reporting failure otherwise.

3.1 Expressiveness of second-order logic

14CHAPTER 3. GENERAL COMPLEXITY OF SECOND-ORDER QUANTIFIER ELIMINATION

Second-order logic often allows for natural formulations of concepts that are awkward or impossible to express in first-order logic. For example, take Leibniz’ definition of equality which stipulates that two objects be identical if they share the same properties. This can be written as

(∗) ∀x, y (∀P (P (x) ⇔ P (y)) ⇒ x = y).

When formalizing equality in first-order logic, this quantification over predicates is commonly simulated by an infinite set of formulas (see [Hod84]):

1. ∀x(x = x)

2. For every first-order formula ϕ the sentence

∀z̄, x, y(x = y ⇒ (ϕ ⇒ ϕ[x/y]))

The variable vector z̄ contains all the free variables in ϕ, which are assumed to be different from x and y. The formulas in the second set express Leibniz’ idea the other way around: if two elements are identical, they can be substituted for each other.

Despite its size, this version only approximates the intended semantics, as it still allows non-standard models of identity that the second-order formulation excludes, cf. [Hod84]. However, it is true in all models with standard identity and logically implies all sentences that are true in such models, which is good enough for many purposes, e.g. automated theorem proving.

Other concepts are not definable in first-order logic at all. A seemingly simple one is finiteness: There is no set of first-order sentences that is verified precisely by those models that have a finite domain. This follows from the compactness property of first-order logic, see [vBD84]. For a secondorder characterization, one may use Dedekind’s criterion that every injective mapping from a finite set to itself if already surjective. Injectivity and surjectivity are readily formalized in first-order logic, and then a formula of the form

∀f(f is injective ⇒ f is surjective)

guarantees the desired finiteness.

This expressiveness is reflected in the theoretical complexity of secondorder logic. It lacks several model-theoretic properties of first-order logic. We mention two that have been chosen by Lindström ([Lin69]) for characterizing first-order logic (see below): compactness and upward Löwenheim-Skolem (for this and more, see [vBD84], for definitions of these properties [Hod84]).

Deduction also becomes much harder. Even in the fragment of Σ_{1}^{1} formulas, universal validity is not an arithmetical notion. Therefore, the set of universally valid Σ_{1}^{1} formulas is not recursively enumerable. Van Benthem and Doets show this in [vBD84], where they also measure the complexity of formulas with arbitrary prefixes. As a consequence, universal validity of second-order formulas can not be axiomatized, as any complete axiomatization together with an effective set of inference rules would again permit a simple enumeration procedure for the valid formulas.

3.2 Characterizing first-order logic

The question naturally arises how we can tell whether we are in the realm of first-order logic. Van Benthem and Doets ([vBD84]) mention essentially three main theorems that have been used in the past to distinguish firstorder from second-order properties.

These theorems characterize first-order logic semantically. They do not directly provide methods for automatically computing first-order equivalents for second-order formulas. Also, they employ model theoretic machinery which is beyond the scope of this work. However, as there can be no algorithm that automatically decides whether a second-order formula has a first-order equivalent for all second-order formulas (see next section), they are indispensable for deciding the remaining cases. Furthermore, they allow us to identify whole classes of second-orderformulas that have first-order equivalents, rather than only single formulas.

To begin with, the aforementioned famous theorem by Lindström answers our question for extensions of first-order logic:

Theorem 3.2.1 (Lindström) Let L be any extension with the two properties:

(a) (Downward Löwenheim-Skolem) If a sentence ϕ of L has an infinite model then it has a model with at most countably many elements.

(b) Either (Upward Löwenheim-Skolem) if a sentence of L has an infinite model, then it has one with uncountably many elements; or (Compactness) if Δ is a theory in L such that every finite set of sentences from Δ has a model then Δ has a model.

Then every sentence of L has exactly the same models as some first-order sentence.

So, instead of any logic with the above properties, we can take first-order logic. However, this does not give a direct answer to the question whether a given property Φ of models is first-order definable. To apply Lindström’s theorem in this case, we would have to construct a logic in which ϕ is represented in the language and which satisfies Lindström’s requirements for logics, as sketched in [vBD84]. Then we could check whether this logic has the above properties.

A theorem by Keisler ([Kei71]) gives a more directly applicable characterization of first-order definable properties. It relies on special models, called ultra products (cf. [BS71]). In addition, we need the notion of elementary equivalence: Two models M_{1}, M_{2} are called elementary equivalent, written M_{1} ≡ M_{2}, if they satisfy the same set of first-order sentences.

Theorem 3.2.2 (Keisler) A property Φ can be defined by a single firstorder sentence iff both Φ and its complement are closed under the formation of isomorphs and ultra products.

However, the ultra product construction is quite abstract. Another characterization of first-order logic by Fraissé ([Fra55]) is of a more combinatorial nature. To state his theorem, we specialize the notion of elementary equivalence of two models. Two models M_{1}, M_{2} are called n-elementary equivalent, written M_{1} ≡_{n} M_{2} if they satisfy the same set of first-order sentences with quantifier rank smaller or equal to n. We call a property Φ of models closed under n-elementary equivalence if for two n-elementary equivalent models M_{1} and M_{2} M_{1} ∈ Φ implies M_{2} ∈ Φ.

Theorem 3.2.3 (Fraissé) A property Φ can be defined by a single firstorder sentence iff it is closed under n-elementary equivalence for some natural number n.

In contrast to the purely semantical characterizations of Keisler and Lindström, the notion of n-elementary equivalence gives a syntactic criterion for the possible complexity of formulas which subdivides the formulas of firstorder logic into equivalence classes. This sometimes allows for proofs that conspicuously exhibit structural properties of models that first-order logic is unable to express, cf. [HET84].

3.3 Computational complexity of reduction

Using the above theorems always requires special proof ideas. They do not provide a uniform, let alone mechanizeable method for deciding whether a given second-order sentence ϕ has a first-order equivalent. The following theorem of Van Benthem and Doets implies that such a method does not exist ([vBD84]):

Theorem 3.3.1 (van Benthem, Doets) The set of Π_{1}^{1} sentences that have a first-order equivalent is not recursively enumerable.

It follows directly that there cannot be an algorithm that decides whether a Π_{1}^{1} sentence can be reduced to a first-order one. For, given such an algorithm, we could recursively enumerate the set of Π_{1}^{1} sentences and filter those that are not reducible, which results in an enumeration contradicting the theorem. So we have

Proposition 3.3.2 There is no algorithm which decides reducibility for Π_{1}^{1} sentences, and therefore no such algorithm for all second-order sentences.

Another observation allows us to establish corresponding results for Σ_{1}^{1} sentences.

Lemma 3.3.1 Let ϕ be a second-order formula. Then ϕ is reducible iff ¬ϕ is reducible.

Proof. Let ψ be a first-order equivalent for ϕ, that is ψ ≡ ϕ. Then ¬ψ ≡ ¬ϕ, ¬ψ first-order, so ¬ϕ is reducible. □

Proposition 3.3.3 There is no algorithm which decides reducibility for Σ_{1}^{1} sentences.

Proof. We show that such an algorithm could be used to decide reducibility of Π_{1}^{1} sentences, which contradicts proposition 3.3.2.

Let ϕ = ∀P̄ϕ′ ∈ Π_{1}^{1}, ϕ′ a first-order sentence, be given. Then

¬ϕ = ¬∀P̄ ϕ′ ≡ ∃P̄ ¬ϕ′ =: φ ∈ Σ_{1}^{1}.

By the above lemma 3.3.1, ϕ is reducible iff ¬ϕ is reducible. So if we could decide reducibility of any ϕ ∈ Π_{1}^{1}, so we can for φ ∈ Π_{1}^{1}, contradicting proposition 3.3.2. □

Proposition 3.3.4 The set of Σ_{1}^{1} that have a first-order equivalent is not recursively enumerable.

Proof. As argued above, an enumeration algorithm could be transformed into an algorithm that decides reducibility. □

Our main concern, however, is not to decide reducibility, but to compute equivalents. More precisely, given a fragment Ω of second-order logic, we would like to have an algorithm RED which always terminates on the input ϕ ∈ Ω and outputs

RED(ϕ) = \{ \begin{matrix}ψ & with ψ ⇔ ϕ and ψ first-order, if ϕ is reducible \\ failure & otherwise \end{matrix}

We call such an algorithm complete on Ω. Such an algorithm can obviously be used to decide reducibility, so it cannot exist if Ω is full second-order logic. We may relax the termination property by allowing the algorithm to run into an infinite loop on non-reducible formulas instead of terminating and reporting failure, obtaining a reduction algorithm PRED with

PRED(ϕ) = \{ \begin{matrix}ψ & with ψ ⇔ ϕ and ψ first-order, if ϕ is reducible \\ undefined & otherwise \end{matrix}

We call PRED semi-complete on Ω. Though this algorithm is less powerful than RED, we could still enumerate the set of reducible formulas ϕ ∈ Ω as follows:

For every natural number n, we enumerate the first n formulas ϕ_{i} ∈ Ω and let the algorithm work for a limited time, say n seconds, on each formula. If it stops with the output ψ, we add ψ to our list. If a formula ϕ ∈ Ω is reducible, the algorithm will eventually add its equivalent as n increases.

We sum this up in

Proposition 3.3.5 Let Ω be a fragment of second-order logic, PRED a semi-complete reduction algorithm Ω. Then the set of reducible formulas ϕ ∈ Ω is recursively enumerable.

Using the above results about non-enumerable fragments of second-order logic, we can deduce

Proposition 3.3.6 There is no semi-complete reduction algorithm for the fragments Π_{1}^{1} and Σ_{1}^{1} of second-order logic.

Proof. By proposition 3.3.5, the existence of this algorithm would imply that the sets of reducible Π_{1}^{1} and Σ_{1}^{1} formulas would be recursively enumerable. But this contradicts proposition 3.3.1 and 3.3.3, respectively. □

For full second-order logic, the consequence is

Corollary 3.3.7 There is no semi-complete reduction algorithm for secondorder logic, i.e., an algorithm which stops on all reducible second-order sentences and outputs an equivalent first-order formula.

Another simple enumeration argument can also show how decidability and reducibility of a fragment of second-order logic are connected in one direction.

Proposition 3.3.8 Let Ω be a recursively enumerable fragment of secondorder logic. If Ω is decidable, then the set of formulas in Ω that have a first-order equivalent in Ω is recursively enumerable.

Proof. Note that we can decide equivalence of two formulas ϕ, ψ in Ω if we can decide tautologies, as ϕ and ψ are equivalent if and only if ϕ ⇔ ψ is a tautology. Now we proceed as above: For every natural number n, we enumerate the first n second-order formulas in Ω. For each of these formulas ϕ, we again enumerate the first n first-order formulas in Ω and check them for equivalence with ϕ by running our decision algorithm for a limited time of n seconds. If an first-order equivalent of ϕ is found, ϕ is printed out.

Now if a formula ϕ has an equivalent ψ in Ω with number m in the enumeration order, the equivalence can be decided in a limited time of n seconds. The above algorithm will find ψ after max(n,m) seconds. □

Note that the algorithm used in the proof can easily be modified to print out the reducible formulas together with their first-order equivalent as tuples. Then, for a given formula, we can reduce it to first-order logic by simply waiting for it to be printed out. If all formulas in Ω are reducible, we only have to wait for a finite time. Thus, for such fragments, we have a reduction algorithm. We will show in 3.4.3 that all propositional formulas with existentially quantified predicates can be reduced to propositional formulas without quantifiers. Therefore, for the set of these formulas, we have a - hopelessly ineffective - reduction algorithm. We will give a simple alternative reduction algorithm for this special case in the proof for 3.4.3.

Now for the converse. How can a reduction algorithm help to decide whether a formula is a tautology? To make the following results directly applicable to the Scan algorithm to be developed in chapter 4, we look at the equivalent problem of deciding whether a formula is satisfiable.

We begin with a simple observation:

Lemma 3.3.2 Let ϕ be a formula of second-order logic, P a vector of predicate symbols. Then ϕ is satisfiable iff ∃P̄ϕ is satisfiable.

Proof. We prove this for the case that P̄ is a single variable. The lemma for longer vectors follows by iterated application of this case.

“⇒”: If ϕ is satisfiable, then there is a model M = ⟨D, I⟩ of ϕ and an assignment A with ϕ^{I,A} = true. Assume that P^{I} = P. Then I = I[P/P], and consequently ϕ^{I,A} = ϕ^{I[P/P],A} = true. So there exists a predicate P over the domain such that ϕ^{I[P/P],A} = true. Then, by definition of the semantics of second-order logic, M satisfies ∃P ϕ.

“⇐”: If ∃P ϕ is satisfiable,there is a model M = ⟨D, I⟩ of ϕ and an assignment A with ϕ^{I,A} = true. So there exists a predicate P over the domain such that ϕ^{I[P/P],A} = true. So the model ⟨D, I[P/P]⟩ satisfies ϕ with the assignment A. □

In the following, we will extensively use the fact that the truth value of the formula ∃P ϕ is independent of the interpretation of P. Intuitively, to decide satisfiability of a sentence ϕ, we first existentially quantify all the predicates it contains, which preserves satisfiability. We then eliminate all these predicates and get an equivalent formula whose satisfiability is easy to decide. A step in this direction is

Lemma 3.3.3 Let ϕ be a sentence of second-order logic which contains only predicates. Let P̄ be a vector of these predicates. Then ϕ is satisfiable iff ∃P̄ϕ is a tautology.

Proof. “⇒”: If ϕ is satisfiable, then so is ∃P̄ϕ, by lemma 3.3.2. But the truth value ∃P̄ϕ is independent of the interpretations of variables and predicates it contains, so if one model satisfies ϕ, then every model satisfies it.

“⇐”: If ∃P̄ϕ is a tautology, it is satisfiable, so by lemma 3.3.2 ϕ is satisfiable, too. □

To make the following more readable, we define a normalization algorithm N ORM that will be used to eliminate redundant predicates that may be introduced during reductions. Let fp(ϕ) be the set of free predicates in ϕ. For arbitrary second-order formulas ψ and ϕ, define N ORM(ϕ, ψ) to be the second-order formula that results from replacing every atom P (t̄) in ψ with P ∉ fp(ϕ) by ⊤. The property of N ORM crucial for our purpose is:

Lemma 3.3.4 If ϕ ≡ ψ, then ϕ ≡ N ORM(ϕ, ψ).

Proof. (sketched) Let P be a predicate symbol in ψ that is not in ϕ. Then the truth value of ϕ does not depend on the interpretation of P. But then the truth value of ψ cannot depend on the interpretation of P, either, as ψ and ϕ are equivalent. So we can interpret P as constantly true, for example, and replace P by ⊤. □

One more point of notation before the next theorem: If Ω is a fragment of first-order logic, let ∃Ω be the smallest fragment of second-order logic such that for every ϕ ∈ Ω, ∃P̄ϕ ∈ ∃Ω.

Theorem 3.3.9 Let Ω be a set of first-order logic sentences without function symbols. Then a reduction algorithm that is complete on ∃Ω can be used as a decision algorithm for Ω.

Proof. Define EVAL to be an algorithm that takes first-order formulas ϕ as input whose only atomic formulas are ⊤ and ⊥ and outputs

EVAL(ϕ) = \{ \begin{matrix}⊤ & if ϕ is a tautology \\ ⊥ & if ϕ is a contradiction \end{matrix}

Such formulas are either tautologies or contradiction, so EVAL is welldefined and total. Obviously, ϕ ≡ EVAL(ϕ). In addition, define CLOSE to be an algorithm which computes CLOSE(ϕ) = ∃P̄ϕ where P̄ is a variable vector consisting of the free variables in ϕ.

Now assume that RED is a reduction algorithm that is complete on ∃Ω. Let ϕ be an arbitrary first-order formula with CLOSE(ϕ) = ∃P̄ϕ. As ∃P̄ϕ is second-order closed, it is either a tautology or a contradiction, so it has a first-order equivalent and RED(∃P̄ϕ) returns a first-order formula. Let RED(ϕ) = ψ. Observe that ϕ contains no free predicates, so N ORM(∃P̄ϕ, ψ) returns a sentence that can only contain ⊤ and ⊥ as atomic formulas. Therefore, EVAL can be applied to it.

We claim that

ϕ ∈ Ω is satisfiable iff N ORMRED(ϕ) = EVAL(N ORM(∃P̄ϕ, ψ)) = ⊤.

We have ∃P̄ϕ ≡ ψ = RED(∃P̄ϕ) by the specification of RED. By lemma 3.3.4, ψ ≡ N ORM(∃P̄ϕ, ψ). Together with the definition of EVAL, we have ∃P̄ϕ ≡ N ORMRED(ϕ) = EVAL(N ORM(∃P̄ϕ, ψ)). Especially, ∃P̄ϕ is a tautology iff N ORMRED(ϕ) is a tautology iff N ORMRED(ϕ) = ⊤.

Now by lemma 3.3.3, ϕ is satisfiable iff ∃P̄ϕ is a tautology iff N ORMRED(ϕ) = ⊤, by the above.

So N ORMRED would be an algorithm for deciding satisfiability in Ω. □

This immediately implies

Corollary 3.3.10 Let Ω be an undecidable fragment of first-order logic. Then there can be no reduction algorithm that is complete on ∃Ω.

Proof. By theorem 3.3.9, a reduction algorithm that is complete on ∃Ω can decide Ω, which is a contradiction. □

We mention one instantiation of this theorem. Let Ω contain all first-order formulas. As first-order logic is undecidable (see, for example [HET84]), there can be no reduction algorithm that is complete on ∃Ω, and as Ω ⊂ Σ_{1}^{1}, there can be no such algorithm for Σ_{1}^{1}.

By examining the proof of theorem 3.3.9, we can obtain a complexity result for reduction algorithms. Let ∥ϕ∥ denote the length of a formula in some representation.

Corollary 3.3.11 Let Ω be a decidable set of first-order sentences without function symbols, and RED a reduction algorithm complete on ∃Ω. Let RED(ϕ) run for at most t_{RED}(∥ϕ∥) deterministic time on every secondorder closed formula ϕ. If ∥RED(ϕ)∥ ≤ sp_{RED}(∥ϕ∥) for all second-order closed formulas ϕ, where sp_{RED} is a polynomial, satisfiability of sentences in Ω can be decided in O(t_{RED}(p(∥ϕ∥)) + q(∥ϕ∥)) time, where q and p are polynomials.

Proof. We show that the algorithm

N ORMRED = EVAL(N ORM(CLOSE(ϕ), RED(CLOSE(ϕ)))) used in the proof of theorem 3.3.9 meets this complexity requirement. We calculate the time consumption for each computation step and sum up at the end.

We assume t_{RED}, sp_{RED}, and each of the time and space bounds given below w.l.o.g. to be monotonous and of course positive polynomials.

Let ϕ be an input formula of length n. It is easy to design CLOSE in such a way that it produces after polynomial time t_{CLOSE}(n) the output ∃P̄ϕ which has a length of at most sp_{CLOSE}(n), sp_{CLOSE} a polynomial in any reasonable representation of formulas.

Let RED(∃P̄ϕ) = ψ, a result computed after t_{RED}(sp_{CLOSE}(n)). By assumption, and by monotonicity of sp_{RED},

∥ψ∥ ≤ sp_{RED}∥∃P̄ϕ∥) ≤ sp_{RED}(sp_{CLOSE}(n)).

N ORM(∃P̄ϕ, ψ) can also compute its result φ in polynomial time when input the two formulas, say t_{N ORM}(∥∃P̄ϕ∥ + ∥ψ∥). φ will usually be the size of ψ, still we may give it polynomial space sp_{N ORM}(∥∃P̄ϕ∥ + ∥ψ∥). Now, by monotonicity and the above,

t_{N ORM}(∥∃P̄ϕ∥ + ∥ψ∥) ≤ t_{N ORM}(sp_{CLOSE}(n) + sp_{RED}(sp_{CLOSE}(n)))
=: uptb_{N ORM}(n)

with uptb_{N ORM} a polynomial (as a composition of polynomials) giving an upper time bound for upb_{N ORM}.

Similarly the output length ∥φ∥ of N ORM is bounded by

∥φ∥ ≤ sp_{N ORM}(∥∃P̄ϕ∥ + ∥ψ∥)
≤ sp_{N ORM}(sp_{CLOSE}(n) + sp_{RED}(sp_{CLOSE}(n)))
=: upsb_{N ORM}(n)

by monotonicity and the above inequalities for ∥∃P̄ϕ∥ and ∥ψ∥.

The job of EVAL can be done in linear time, we bound it by the polynomial t_{EVAL}. On φ, it runs for t_{EVAL}(∥φ∥) ≤ t_{EVAL}(upsb_{N ORM}(n)).

As total running time we have

t_{N ORMRED}(n)
= t_{CLOSE}(∥ϕ∥) + t_{RED}(∥∃P̄ϕ∥) + t_{N ORM}(∥∃P̄ϕ, ψ∥) + t_{EVAL}(∥φ∥)
≤ t_{CLOSE}(n) + t_{RED}(sp_{CLOSE}(n))
+uptb_{N ORM}(n) + t_{EVAL}(upsb_{N ORM}(n))
= t_{RED}(sp_{CLOSE}(n)) + t_{CLOSE}(n)
+uptb_{N ORM}(n) + t_{EVAL}(upsb_{N ORM}(n))
= t_{RED}(p(n)) + q(n)

for p =^{def} sp_{CLOSE} and q =^{def} t_{CLOSE} + uptb_{N ORM} + t_{EVAL} ∘ upsb_{N ORM}.

p and q are sums of compositions of polynomials and therefore polynomials themselves. This proves our claim. □

The seemingly strange condition on the complexity of the output of RED is necessary for the polynomial time transformation of a satisfiability problem into a reduction problem. This in turn allows for the following consideration. If t_{RED},p and q are polynomials, then so is t_{RED} ∘p+q. That is, if formulas in ∃Ω can be reduced in polynomial time, satisfiability in Ω can be decided in polynomial time. But, taking Ω to be the set of propositional formulas, a polynomial time reduction algorithm would imply a polynomial time decision algorithm for satisfiability of propositional formulas. Such an algorithm has not been found until today. Its existence would prove P = N P. This clearly shows the depth and complexity of problems involved in the development of reduction algorithms.

3.4 Reducible fragments of second-order logic

In this section, we list some reducible fragments of second-order logic that have a simple syntactic form. For one of them, the fragment of quantified propositional formulas in Σ_{1}^{1}, we give a simple reduction algorithm.

Theorem 3.4.1 Let ϕ be a quantifier free formula of first-order logic. Then

1. all formulas of the form ∃P̄∃ȳ ϕ(P̄) are reducible to a single first-order sentence.

2. all formulas of the form ∃P̄∀ȳ ϕ(P̄) are reducible to a set of possibly infinite disjunctions of first-order formulas.

Proof. Both statements are proven in [vBD84]. □

To see the coverage of these fragments, it is useful to consider the following normal form, which is basically skolem normal form with skolem functions replaced by existentially quantified predicates:

Proposition 3.4.2 For any formula ϕ ∈ Σ_{1}^{1} of second-order logic, an equivalent formula of the following form can effectively be found:

∃P̄∀x̄∃ȳ ψ(P̄, x̄, ȳ)

where ψ is quantifier free. If all predicates in ϕ have zero arity (i.e., they are propositional variables), ψ can be chosen as a formula of propositional logic.

Proof. See [vB83]. □

Together with the following lemma, this will allow any easy proof of the reducibility of Σ_{1}^{1} formulas with only 0-place predicates.

Lemma 3.4.1 Let ϕ(P) be a formula of second-order logic, and P a 0-place predicate. Then

∃P ϕ(P) ≡ ϕ(⊤) ∨ ϕ(⊥)

where ϕ(⊤) (ϕ(⊥)) is the formula that results from replacing all occurrences of P in ϕ by ⊤ (⊥).

Proof. By structural induction. □

Theorem 3.4.3 Any formula ϕ ∈ Σ_{1}^{1} in which all occurring predicates are 0-place can effectively be reduced to a formula of propositional logic.

Proof. We assume w.l.o.g. that ϕ is in the normal form of proposition 3.4.2, i.e., ϕ is given as

∃P_{1}, …, P_{n} ∀x̄∃ȳ ψ(P̄, x̄, ȳ)

with ψ a quantifier free formula of propositional logic. Then there can be no free first-order variables in ψ, so we eliminate the first order quantifiers, resulting in

∃P_{1}, …, P_{n}ψ(P̄, x̄, ȳ).

Now we successively apply lemma 3.4.1: we replace the subformula ∃P ψ(P̄, x̄, ȳ), by the equivalent formula without P obtained by lemma 3.4.1. The same is done for the other quantified predicates, until we have a propositional formula without quantifiers that is equivalent to ϕ. □

Scan: Elimination of existentially quantified predicates

In this chapter, we will formulate a special quantifier elimination problem and present the Scan algorithm as a possible solution to this problem. Several extensions of the algorithm will improve its termination properties.

4.1 The basic Scan algorithm

The Scan algorithm tackles the following problem: given a second-order formula Φ(P̄) = ∃P̄ϕ, ϕ a first-order formula, find a (possibly infinite) set ψ of first-order formulas such that

∃P̄ϕ ≡ ψ.

As is shown in [Ack35a], [Ack35b], this problem is solvable. Indeed, Scan is able to solve it, as the algorithm always generates a set ψ with the above properties. However, Scan does not always find a finite ψ when there is one. This would make Scan a semi-complete reduction algorithm for the fragment Σ_{1}^{1} of second-order logic as defined in section 3.3. By proposition 3.3.6, such an algorithm cannot exist.

4.1.1 A basic version

The main idea of Scan is quite simple: Scan generates a set of firstorder consequences of a formula that is strong enough to imply the formula itself. This approach can be motivated by a simple observation. Assume we are given a formula Φ(P̄) and want to find an equivalent formula set ψ with Φ(P̄) ≡ ψ as above. If ψ exists, then it can be found in the set of all first-order consequences of Φ(P̄), that is, the set {ψ | ψ ⊧ ψ and ψ is a first-order formula} This set in turn of course implies ∃P̄, for it contains ψ, and ψ ⊧ Φ(P̄). So we may try to solve the problem by computing the set of first-order consequences of Φ(P̄) and hope that they are equivalent to this formula. However, as this set is usually infinite and full of redundancies, we should be content with a, hopefully finite, representation with few redundancies.

4.1.1.1 Preliminaries

Techniques for drawing consequences from clause sets without too much redundancies and removing redundancies from the set have been developed in the area of first-order theorem proving, and to some extent, they can be carried over to the problem of second-order quantifier elimination. In particular, the well-known resolution rule, invented by Robinson ([Rob65]), can be modified to yield the so-called C-resolution used in Scan to draw consequences from clauses. The C-resolution inference rule (C for constraint) has the following form:

Definition 4.1.1 (C-resolution) Let C = P (s_{1}, …, s_{n})} ∨ C′ and D = P (t_{1}, …, t_{n})} ∨ D′ be two clauses with disjoint variable sets. Then the rule

\frac{P (s_{1}, …, s_{n}) ∨ C′ ¬P (t_{1}, …, t_{n}) ∨ D′}{C′ ∨ D′ ∨ s_{1} ≠ t_{1} ∨ … ∨ s_{n} ≠ t_{n}}

is called C-resolution rule.

We denote the C-resolvent by CRes(C, P (s_{1}, …, s_{n}), D, P (t_{1}, …, t_{n})). Note that C-resolution can always be performed on complementary literals, whereas ordinary resolution requires the literals to be unifiable.

Classical factorization is modified to C-factorization analogously:

Definition 4.1.2 (C-factorization) Let C = P (s_{1}, …, s_{n}) ∨ P (t_{1}, …, t_{n}) ∨ C′. Then the rule

\frac{P (s_{1}, …, s_{n}) ∨ P (t_{1}, …, t_{n}) ∨ C′}{P (s_{1}, …, s_{n}) ∨ C′ ∨ s_{1} ≠ t_{1} ∨ … ∨ s_{n} ≠ t_{n}}

is called C-factorization rule.

28CHAPTER 4. SCAN: ELIMINATION OF EXISTENTIALLY QUANTIFIED PREDICATES

A C-factor of C is denoted by CF ac(C, P (s_{1}, …, s_{n}), P (t_{1}, …, t_{n})).

Some more definitions will abbreviate standard applications of these inference rules to clause sets. They extend the rules from predicates to clauses to sets on each argument.

Dealing with quantifier elimination, we will often be given a set or a vector of predicate variables P̄. Again, we will avoid notational overhead by treating vectors as sets and vice versa, e.g. we will write “P′ ∈ P̄” instead of “P′ is a component of the vector P̄”.

For a clause C, we let CF ac(C) denote the set of all factors obtained by one application of factorization on predicates in P̄. Formally,

CF ac(C, P̄) =^{def} \{CF ac(C, P′(t̄), P′(s̄)) | {C = P′(t̄) ∨ P′(s̄) ∨ \atop R for some P′ ∈ P̄\}.}

The straightforward extension to clause sets M is

CF ac(M) =^{def} ⋃_{C∈M} CF ac(C).

We need the closure of a clause set under factorization with respect to a vector of predicates P̄. To this end, define

CF ac^{1}(C, P̄) =^{def} CF ac(C, P̄) and CF ac^{i+1}(C, P̄) =^{def} CF ac(CF ac^{i}(C, P̄)).

Then

CF ac^{∞}(C, P̄) =^{def} ⋃_{i∈IN} CF ac^{i}(C, P̄)

computes all recursive factors of a clause. Finally, for a clause set M,

CF ac^{∞}(M, P̄) =^{def} ⋃_{C∈M} CF ac^{∞}(C, P̄)

is the closure of M under factorization.

Similar notions are defined for C-resolution. For two clauses C and D, let CRes(C, D) denote the set of all resolvents computed by a single application of the C-resolution rule on C and D. Extended to clause sets M,

CRes(M) =^{def} ⋃_{C,D∈M} CRes(C, D).

Canonically, CRes^{1}(M) =^{def} CRes(M), CRes^{i+1} =^{def} CRes(CRes^{i}(M)).

Slightly different from the C-Factorization case, CRes_{Σ}^{1}(M) =^{def} CRes(M), CRes^{i+1} =^{def} CRes(CRes^{i}(M)) ∪ CRes^{i}(M). Now the closure is formed by CRes^{∞}(M) =^{def} {C | C ∈ CRes_{Σ}^{i}(M) for some i ∈ IN}. Then we set

CRes^{∞}(M) =^{def} ⋃_{C∈M} CRes^{i}(C).

An important operation will resolve one literal L in a clause C = L∨C′ with all complementary literals in a clause set M. We define CRes(C, L, M) =^{def}

{CRes(C, L, D, ¬L) | D = ¬L ∨ D′}, CRes_{Σ}^{1}(C, L, M) =^{def} CRes(C, L, M),

CRes_{Σ}^{i+1}(C, L, M) =^{def} CRes(C, L, CRes_{Σ}^{i}(C, L, M)) ∪ CRes_{Σ}^{i}(C, L, M), and

then

CRes^{∞}(C, L, M) =^{def} {C | C ∈ CRes_{Σ}^{i}(C, L, M) for some i ∈ IN}.

At last, we formally define the closure CInf^{∞} of a clause set under the C-inference rules C-factorization and C-resolution on predicate symbols from a vector. Note that we exclude self-resolution of clauses. Let CInf^{∞}(M, P̄) be the smallest set S such that C_{1}[P (t̄), C_{2}[¬P (s̄)] ∈ S, C_{1} ≠ C_{2} implies CRes(C_{1}, P (t̄), C_{2}, ¬P (s̄)) ∈ S, and C[P (t̄), P (s̄)] ∈ S implies CF ac(C, P (t̄), P (s̄)) ∈ S.

4.1.1.2 The algorithm

Now we are prepared for a defining and explaining a first version of the Scan algorithm. It takes as an input a second-order formula ∃P̄ϕ and outputs, if it terminates, a first-order or second-order formula ψ with ψ ≡ ∃P̄ϕ.

In the following, given some variable vector P̄, we say that a clause C is a P̄-clause if it contains a predicate P′ ∈ P̄. See figure 4.1 for the algorithm. The deletion of a clause C with a literal L from a clause set M = C ∪R that has been resolved with the rest of the clause set R is called purity deletion, the literal itself and the clause C are called pure. Note that, to be pure, a literal is not required to be resolved with literals in the clause it is contained in. In other words, self-resolution of clauses in Scan is not necessary, though correct.

The algorithm can be subdivided into three phases:

1. Normalization: ϕ is converted into a clause set M = CNF (ϕ), possibly by introducing skolem functions

2. Elimination: M is transformed into a new clause set M′ not containing the existentially quantified predicates Algorithm 4.1.3 (Basic SCAN)

formula Scan( formula ∃P̄ϕ)

set<clause> M;

Let M = CNF (ϕ);

While (There is some P̄-clause C ∈ M){ // Nondeterministically generate all C-factors and C-resolvents of a particular literal

If (There are two distinct clauses C[P′(t̄)], D[P′(s̄)] such that

CRes(C, P′(t̄), D, ¬P′(s̄)) ∉ M) then Let M = M ∪ CRes(C, P′(t̄), D, ¬P′(s̄)); If (There is a clause C[P′(t̄), P′(s̄)] such that

CF ac(C, P′(t̄), P′(s̄)) ∉ M) then Let M = M ∪ CF ac(C, P′(t̄), P′(s̄)); // If all resolvents with a literal have been generated, delete clause If (C[P′(t̄)] ∈ M, M = C ∪ R, (CRes^{∞}(C, P′(t̄), R) ∪ CF ac^{∞}(C, P̄)) ⊂ M) then Let M = R; }

// Eliminate skolem functions

Let ψ = Usk(M);

Return(ψ);

Figure 4.1: The basic Scan algorithm

3. Unskolemization: M′ is transformed into a formula ψ without skolem functions

Each phase deserves some explanation, especially about how the normalization and unskolemization steps preserve equivalence.

Normalization The normalization operation is standard in many firstorder theorem provers. There, it is commonly used as an satisfiability preserving operation, i.e., ϕ is satisfiable iff CNF (ϕ) is satisfiable. However, many algorithms for computing clause normal form do something stronger, namely, they compute CNF (ϕ) such that ϕ ≡ ∃f̄∀x̄ CNF (ϕ), where f̄ is the vector consisting of all the skolem functions introduced for generating the normal form, and x̄ consists of all free variables in the clause set. In chapter 5, this interpretation is justified and examined more closely. We assume that CNF (·) satisfies the above equivalence, which implies

∃P̄ϕ ≡ ∃P̄∃f̄∀x̄ CNF (ϕ) = ∃P̄∃f̄∀x̄ M.

Elimination The elimination process does the main work of the algorithm. Note that by the CNF transformation, the clause set now contains the existentially quantified predicates of ϕ without explicit quantification, so that C-resolution and C-factorization can be applied. This may be seen as a kind of skolemization of predicates. In essence, the elimination step computes the closure of the clause set under C-resolution and C-factorization and afterwards deletes all clauses not containing any of the existentially quantified predicates. If the closure is finite, then the second step terminates, and we have

∃P̄∃f̄∀x̄ M ≡ ∃P̄∃f̄∀x̄ M′ ≡ ∃f̄∀x̄ M′.

The second equivalence holds because M′ does not contain any clauses with predicates in P̄.

Unskolemization The last phase now gets a clause set M′ with ∃f̄∀x̄ M′ ≡ ∃P̄ϕ, f̄ containing all skolem functions. To get a regular firstorder formula without skolem functions, we have to turn them back into existential quantifiers. E.g., let f be a skolem function and assume that the output of the elimination phase is M = {G(f(x), x)}. We interpret this clause as the formula ∃f∀x G(f(x), x), which can be seen as a the result of skolemizing ∀x∃z G(z, x). We call this process of reversing skolemization unskolemization. Chapter 5 deals with this problem.

We will use Scan(Φ) to denote the result of Scan applied to a secondorder formula Φ. In addition, we will need to talk about the elimination phase of Scan alone, which gets as input a clause set (resulting from the CNF transformation of Φ) and outputs a clause set, without subsequent unskolemization. The result of this phase is Scan(M), where M is a clause set. We take this set to be defined, even if Scan does not terminate. In this case, Scan(M) is the set that Scan enumerates. Note that this set does not contain any clause with an existentially quantified predicate, as all such clauses are pure and therefore deleted.

An example illustrates how the algorithm works. Let

Φ = ∃P ϕ = ∃P ∃z_{1}, z_{2} (Q(z_{1}) ⇒ P (z_{1})) ∧ (P (z_{2}) ⇒ Q(z_{2})).

We translate the implication connectives and turn the existential quantifiers into skolem constants a and b to obtain the clause set

M =^{def} CNF (ϕ) = {C_{1} =^{def} ¬Q(a) ∨ P (a), C_{2} =^{def} ¬P (b) ∨ Q(b)}.

One C-resolution of C_{1} with C_{2} yields

C_{3} =^{def} CRes(C_{1}, P (a), C_{2}, ¬P (b)) = Q(a) ∨ Q(b) ∨ a ≠ b

C_{1} is now pure and can be removed from M, leaving M = {C_{2}, C_{3}}. There are no further resolution possibilities for the literal ¬P (b) ∈ C_{2} with literals in M, so it is pure, and we can delete C_{2} from M,too. Now M = {C_{3}}.

Finally, we unskolemize M. Let

ψ = Usk(∃a, b Q(a)) = ∃z_{1}, z_{2} Q(z_{1}) ∨ Q(z_{2}) ∨ z_{1} ≠ z_{2},

where z_{1}, z_{2} are first-order variables. To sum it up, we have the following chain of equivalences:

∃P ϕ
≡ ∃P ∃a, b M  by properties of CNF
≡ ∃P ∃a, b C_{3}  by correctness of Scan
≡ ∃a, b C_{3}  as P has no occurrence in C_{3}
≡ ∃z_{1}, z_{2} Q(z_{1}) ∨ Q(z_{2}) ∨ z_{1} ≠ z_{2} as ∃a, b C_{3} ≡ Usk(∃a, b C_{3})

4.1.2 Properties of the basic algorithm

The Scan algorithm is proven correct and, with a generalized notion of soundness explained below, also sound in [GO92]. Correctness of Scan guarantees that every output formula of Scan is equivalent to the input formula, in short Scan(∃P̄ϕ) ≡ ∃P̄ϕ.

Completeness of Scan would imply that the algorithm would be capable of computing a first-order equivalent for all input formulas. This is simply impossible because such an equivalent does not exist for every formula in the considered input class, c.f. section 3.1. A relaxed condition is to require an equivalent formula for those cases where it exists. But this is an requirement that would make Scan a semi-complete reduction algorithm as defined in 3.3 for all formulas of the form ∃P̄ϕ. However, these formulas make up the fragment Σ_{1}^{1} of second-order logic, and proposition 3.3.6 states that a semi-complete reduction algorithm cannot exist for this fragment.

We can escape these negative results by taking as the output of Scan the set M of clauses that it enumerates, ignoring whether Scan terminates or not. Recall that we denoted this set by Scan(M). In [GO92] the authors deduce from results of Ackermann ([Ack35a],[Ack35b]) that the set of clauses in the closure that do not contain any of the existentially quantified variables is equivalent to the clause normal form of the input formula. Therefore, Scan is complete in the sense that, on any input clause set, it enumerates a clause set equivalent to the initial clause set which does not contain predicate variables.

More formally, let P̄ be the vector of existentially quantified predicates in a clause set M. Then

∃P̄∀x̄ M ≡ ∃P̄∀x̄ Scan(M) ≡ ∀x̄ Scan(M).

Keeping in mind the theoretical limitations discussed above, this is in some sense optimal.

Note, however, that the set Scan(M) does not represent a first-order formula as long as it contains skolem functions, which it usually does. Therefore, to obtain a first-order formula, we also have to eliminate those skolem functions. So it depends heavily on the final unskolemization step, whether Scan finally outputs a first-order formula. Not surprisingly, there can be no unskolemization algorithm that transforms any Scan output clause set into am equivalent first-order formula, or even an equivalent set of first-order formulas. This would again imply that there exists a first-order equivalent for every Scan input formula Φ ∈ Σ_{1}^{1}, which is not true, as discussed in section 3.1.

We sum this up in

Theorem 4.1.4 (Gabbay, Ohlbach) The Scan algorithm is correct and complete in the following sense: Let M be a clause set, interpreted as a formula ∃P̄∃f̄∀x̄ M. Then there exists a (possibly infinite) clause set M′ such that ∃P̄∃f̄∀x̄ M ≡ ∃P̄∃f̄∀x̄ M′, and Scan enumerates such a clause set, i.e.,

∃P̄∃f̄∀x̄ M ≡ ∃f̄∀x̄ Scan(M).

The core of the proof is the correctness proof of the following purity deletion rule.

Lemma 4.1.1 (Gabbay, Ohlbach) Let M be a clause set, C ∈ M a clause and L ∈ C a literal with L = P or L = ¬P for some predicate symbol P that is interpreted as existentially quantified. If M contains all C-factors of C and all C-resolvents of C with some other clause in M on L, then C is called pure, and removing C from M preserves equivalence. Formally,

∃P M ≡ ∃P (M \ C) ∪ CRes(C, L, M) ∪ CF ac^{∞}({C}, {P })

The purity deletion criterion, which demands the presence of all C-factors and C-resolvents on a selected literal will play an important role in the next section, where it will be used for proving the correctness of the extended Scan algorithm.

4.2 Extensions of the basic algorithm

Using the Scan algorithm, we have to deal with problems well known from automated theorem proving: exponentially growing clause sets, generation of redundant clauses, non-termination of the procedure and many more. Fortunately, some techniques that have been developed in the field of automated theorem proving for handling those problems can be carried over to our problem of quantifier elimination. As theorem provers are usually based on a calculus, there are two straightforward ways to improve them:

• by adding new inference rules

• by changing the inference strategy

We will extend Scan mainly by adding new inference rules and do not explore inference strategies. For discussing the new rules, we will even fix an inference strategy, which is similar to the one used in the implementation of Scan. However, the new rules cannot be arbitrarily combined with the purity deletion rule, which will impose restrictions on possible inference strategies.

We separated the presentation of the extended Scan algorithm and the sketch of its correctness proof (section 4.2.3), as the proof is technically awkward and does not provide much intuitive insight.

4.2.1 Simplification rules

All simplification rules presented in this section transform clause sets into equivalent clause sets which are smaller. In general, this makes a clause set more readable, and, as a computational advantage, also saves space, which are both desirable effects. However, our primary intention is to use simplification rules for making Scan terminate on a larger class of secondorder formulas than it does in its basic version by avoiding loops. This is crucial, as Scan may loop on even very simple input formulas:

Example 4.2.1 Consider the following clause set:

1. ¬P (x) ∨ P (f(x)) ∨ R(f(x))

2. P (a)

3. R(f(a)))

Assume we choose the literal ¬P (x) in clause 1 as the literal to purify. It has no C-factors and so we start by resolving it with clause 2, resulting in clause 4: P (f(x)) ∨ R(f(x)) ∨ x ≠ a, which we replace by the equivalent P (f(a)) ∨ R(f(a)) (Intuitively correct as it seems, this step must be justified, which is explained and done below). We choose this clause as the new resolution partner and obtain clause 5: P (f(f(x)) ∨ R(f(f(x))) ∨ x ≠ a ∨ R(f(a)), again simplifying this to P (f(f(a))) ∨ R(f(f(a))) ∨ R(f(a)). If we continue this way, always resolving with the last resolvent, we get the P (f^{n}(a)) ∨ ⋃_{i=1}^{n} R(f^{i}(a)) as clause number 3 + n, and get caught in an infinite loop. Of course we might avoid this loop by starting with another clause as the pure clause. But on more complex clause sets, things might not be so obvious. In fact, there can be no ’perfect’ inference strategy for SCAN that avoids all loops simply for the reason that no second-order quantifier algorithm is complete and inevitably loops on some input formulas. In this special case, we can alternatively apply a simplification rule: Note that clause 3 R(f(a)) subsumes the first resolvent. We will show in section 4.2.3 that, in this case, we do not have to generate the C-resolvents of a resolvent that is subsumed by another, so we may stop and delete clause 1, which is now pure in a wider sense. It is not pure in the sense of the definition, as not all resolvents of clause 1 with clause 2 are present, though they are implied, as they all would contain the literal R(f(a)) of clause 3 and therefore be subsumed.

In the above example, it is clear that deletion of subsumed clauses preserves equivalence of a clause set. It is not at all obvious, however, that the deletion of clause 1 is equivalence preserving, because it is not pure in the sense of lemma 4.1.1. This is possible because the C-resolvents of the subsuming clause (none in this case) will subsume the C-resolvents of the subsumed clause, which is proven in section 4.2.3. So the C-resolvents of the subsumed clause are “virtually” present and we may still delete the pure clause - provided that the C-resolvents of the subsuming clause have been generated. Therefore, given an equivalence-preserving transformation rule for clause sets, we face the question how it interplays with the purity deletion rule, that is, which C-resolvents have still to be generated after the transformation.

The example also shows the hallmark of loops: recursive clauses, that is, clauses containing the literal selected for purification and its negation. It is easy to see that only the purification of recursive clauses leads to loops. Consequently, we will try to eliminate them.

We will now describe equivalence preserving transformation rules for clauses and clause sets and place them in a new extended Scan algorithm, interplaying with the purity deletion rule.

4.2.1.1 Equivalence preserving transformation rules on clauses

C-resolution and c-factoring produce a lot of inequalities which can easily be eliminated by the following proposition.

Proposition 4.2.2 For any first-order clause ϕ and term t, where t does not contain x,

∀ȳ ϕ_{{x↦t}} ≡ ∀x∀ȳ ϕ ∨ x ≠ t

in all standard models of equality, where y is a variables vector containing all variables in ϕ and t.

For an arbitrary term t, we call a constraint x ≠ t non-recursive if t = x or t does not contain x. We use the above proposition to define an operation that eliminates all non-recursive constraints in a clause.

Definition 4.2.3 (Constraint elimination) Let C be a clause. Then we define CtEl(C) to be a clause that results from eliminating all non-recursive constraints from C by repeatedly applying proposition 4.2.2.

From proposition 4.2.2 it is obvious that

C ≡ CtEl(C).

This constraint simplification makes clauses more readable and facilitates subsumption on clauses. For example, P (a) does not subsume C =^{def} P (x) ∨ x ≠ a, while it trivially does subsume P (a) = CtEl(C).

Another simplification rule is condensing, known from the field of theorem proving, a combination of standard factoring and subsumption that shortens clauses. We again assume a linear order on the set of clauses to obtain uniqueness in the following definition.

Definition 4.2.4 (Condensing) Let C be a clause, F be a factor of C obtained by an arbitrary number of binary factorizations with the following properties:

• F ⊴ C

• there is no factor of C with less literals which subsumes C • in the linear order on clauses, F is the smallest of all factors which

have the above two properties.

We define

Cond(C) =^{def} F.

By correctness of factorization, it is clear that

C ⊧ F = Cond(C),

and by the properties of subsumption we have

F ⊧ Cond(C),

combining to C ≡ Cond(C).

Note that we do not restrict factorization to quantified predicates. Syntactically, condensing can be done by instantiating a clause and deleting all those literals that become redundant by a subsumption. For example, Cond(A(x) ∨ A(b) ∨ R) = A(b) ∨ R.

4.2.1.2 Equivalence-preserving transformation rules on clause sets

If M is a clause set and C a clause such that M ⊧ C, then of course M ∪ C ≡ M. In other words, we may delete clauses that are implied by the rest of the clause set. As two special cases, we may delete subsumed clauses, which are implied by a single other clause, and tautologies, which are implied by the empty clause set. These special cases have the pleasant property that they are decidable on first-order clause sets, while implication is only semi-decidable. Therefore, in any real-world implementation of Scan, we can only approximate the full deletion rule by trying to prove clauses in a limited time or with limited space. Otherwise, we might reintroduce the infinite loops that we wanted to avoid.

A combination of resolution and subsumption leads to the unit-deletion rule.

Definition 4.2.5 Let M be a clause set, C a clause. Let U be the set of all unit clauses in M matching some literal in C:

U = {D ∈ M | D = L_{D} for some literal L,

and νL_{D} = ¬L_{C} for some literal L_{C} ∈ C and some matcher ν}

Let S the subset of all literals in C that are matched by some literal in U. We define

UnitDel(C, M) = C \ S.

Proposition 4.2.6 For a clause set M and a clause C, we have

M ∪ C ≡ M ∪ UnitDel(C, M).

Proof. (Sketch) Let D ∈ M be a unit D = L_{D} such that νL_{D} = ¬L_{C} for some literal L_{C} ∈ C = L_{C} ∨ R and some matcher ν. We resolve (standard resolution) on L_{D} and L_{C} using the matcher as the most general unifier, and obtain the resolvent R, which back subsumes C, because the matcher does not instantiate variables in C. Deletion of subsumed clauses preserves equivalence, and by repeated resolutions with all units in U, we arrive at the equivalent clause set M ∪ UnitDel(C, M). □

The next simplification is very powerful, as it can eliminate a quantified predicate from a clause set completely in one step. It can be seen as an application of the purity deletion rule with a certain inference strategy on clause sets with a special structure. Therefore, it is labeled extended purity rule. To define and prove it, it is useful to define the notion of polarity of a clause. Let P be a predicate. We say that a clause C containing occurrences of P has positive polarity in P if it only contains positive occurrences of P, and negative polarity if it only contains negative occurrences of P. C has mixed polarity in P if P occurs both positively and negatively, and neutral polarity in P if P does not occur in C at all. Define

P ol(P, C)) =^{def} \{ \begin{matrix}1 & if P occurs in C, and C has positive polarity in P \\ 0 & if P has neutral or mixed polarity in C \\ −1 & if P occurs in C, and C has negative polarity in P \end{matrix}

Two clauses C, D have opposite polarity in P if P ol(P, C) · P ol(P, D) = 1. For the definition, recall that \overline{proj}_{P} (M) denotes the set of all clauses in M not containing the predicate symbol P.

Definition 4.2.7 Let M be a clause set and P a predicate symbol. We say that P is polarity-pure or p-pure in M if it does not contain two clauses that have opposite polarity in P. We define

ExtP urify(P, M) = \{ \begin{matrix}\overline{proj}_{M}(P) & if P is p-pure in M \\ M & otherwise \end{matrix}

Proposition 4.2.8 For any clause set N and predicate symbol P,

∃P ∀x̄ N ≡ ∃P ∀x̄ ExtP urify(P, N)

Proof. This is obvious in case that P is not p-pure, as nothing changes. Assume that P is p-pure. It is clear that

∀x̄ N ≡ ∀x̄ \overline{proj}_{N}(P),

so that by monotonicity of the formula ∃P ∀x̄ϕ we conclude

∃P ∀x̄ N ≡ ∃P ∀x̄ ExtP urify(P, N).

For the other direction, we assume that N contains only clauses C with P ol(P, C) = 1 or P ol(P, C) = 0. The case P ol(P, C) = −1 or P ol(P, C) = 0 is alike. Now assume we are given a model ⟨D, I⟩ for \overline{proj}_{N}(P). We have to show that in this model there is an interpretation of P such that M ⊧ ∀x̄N. We choose P^{I,A} = D, that is, P is constantly interpreted as true. It is obvious that this interpretation meets the requirement, which completes the proof. □

With these simplification rules at hand, we may define an improved version of Scan.

4.2.2 The extended Scan algorithm

The extended Scan algorithm XScan uses all simplification rules presented in the last section. It also removes some non-determinism of the basic version by employing a simple inference strategy:clauses are purified successively. That is, a clause and a literal within this clause is selected, all C-factors of this clause and C-resolutions with other clauses are generated, and the clause is deleted before C-resolutions with or C-factors of other clauses are generated.

We already pointed out that simplification rules relieve us from building C-resolutions with certain clauses. We will attach marks to clauses that must be resolved against the selected clause by the function mark(), and test them for marks with the boolean function marked(). Marks are removed with unmark(), and we assume them to disappear if the clause they mark is deleted. These functions are extended to sets by member-wise application. See figure 4.2 for the algorithm. The procedure Process contains all simplification rules but the extended purity rule. It appends the simplified clause to the clause set given as parameter, if it is not redundant. If the Algorithm 4.2.9 (Extended Scan)

formula XScan( formula ∃P̄ϕ) set<clause> M; Let M = CNF (ϕ); // While there are clauses with quantified predicates For (All P ∈ P̄) M = ExtP urify(P, M); While (there is a P̄-clause P ureCl){

Let M = M \ P ureCl; Select a literal P ureLit ∈ P ureCl built from a quantified predicate P; Let M = M ∪ CF ac^{∞}(C,P); // mark all resolution parters For (All clauses D ∈ M with ¬P ureLit ∈ D) mark(D); While (There is a clause D with marked(D) = true){

For (All resolvents Res = CRes(P ureCl, P ureLit, D, L′)) Do { // check Res for redundancy, simplify and mark // see below for procedure Process (Res, M, PureCl) Process(Res, M, P ureCl); } // Purify if predicate is extended pure M = ExtP urify(P, M); }

}; // Eliminate skolem functions Let ψ = Usk(M); Return(ψ);

Figure 4.2: The extended Scan algorithm clause P ureCl is back subsumed by one of its C-resolutions, all clauses in M are unmarked, and the purification of P ureCl thus stopped.

Algorithm 4.2.10 (Process)

Process( clause Res, set<clause> M, clause P ureCl) // Simplify resolvent Res = UnitDel(Res, M); Res = Cond(Res); // Append Res to M if it is not redundant If (Res is not a tautology and not M ⊧ Res) M = M ∪ Res; // Collect clauses that are (back) subsumed by Res Let B = {C ∈ M | Res, C ⊴}; Let M = M \ B; If (Res ⊴ PureCl) unmark(M); Return;

4.2.3 Properties of the extended version

Due to lack of time, I could not give a proof of the correctness of XScan. However, I try to sketch how such a proof might look like, and what pitfalls one has to avoid. For simplicity, we will use a modified version of the main loop of XScan, which has slightly different marking and uses labeled clauses.

4.2.4 Modeling XScan inference

We model the XScan algorithm as follows. We will investigate the situation that a pure clause pure is given and successively resolved with a clause set M, and that simplification rules are applied. Now we look at the algorithm in figure 4.3: Note that we directly add newly generated clauses to the clause set, and then apply simplifications to the clause set, instead of adding them when they could not be proven redundant. This can model even further extensions of the XScan algorithm. We denote the marking function by α for notational convenience. All clauses that have not been resolved upon carry a mark, written α(C) = 1 for marked clauses. We assume for simplicity that all unresolved clauses carry marks, as opposed to the situation in XScan, which marks only possible resolution partners with literals complementary to the pure literal. α(M) denotes the set of all clauses in M that are marked, \overline{α}(M) the complement. Note that all of 1. Mark all clauses in M.

2. While there are marked clauses:

Non-deterministically, either

• Pick a marked clause C and add

all its C-resolvents R with pure to M,

unmark C, mark R

• or apply a simplification rule to M

Figure 4.3: A model for XScan

the following could be transferred to the case of a literal marking function, which would allow for finer control.

As one parent in each resolution step always is pure, we write CRes(C) for CRes(pure, C), similarly for other resolution functions. Then by X(M), given our marking function α, we denote the set \overline{α}(M) ∪ CRes(α(M)). X(M) denotes the set that XScan would compute if there were no further simplifications. We write Xα if we want to emphasize that X depends on a marking function.

We assume that all clauses that have been generated by a C-resolution step are labeled with their parent clause (which was resolved with pure), which distinguishes clauses with the same set of literals by their parents. That is, strictly speaking, we operate on tuples, or on proof trees, and have to lift, for example, subsumption to this structure. However, we hope that the following is clear without these formal details.

4.2.5 A loop invariant

We want to show that after each transformation of the set M into a set M′, we have

Xα(M) ≡ Xα′(M′),

with a new marking function α′. If the algorithm terminates with some M and α, α(M) must be empty, and we would have X(M) = \overline{α}(M), which by a chain of equivalences leads to the closure of the original clause set M_{0}, since, for M_{0}, X(M_{0}) = CRes(M), because all clauses in M_{0} are marked. It then remains to be shown how this simulates XScan. The main point is that XScan cannot distinguish between two clauses that have the same set of literals but are derived from different parents, whereas we can do this using the labels. Hence, a bijective mapping from the set of generated labeled clauses to the set of clauses does not necessarily exist. However, we can use the subsumption elimination rule to remove copies of clauses with different labels, which modulo some technical details makes the set of labeled “homomorphic” to the set of clauses in XScan.

4.2.6 Studying subsumption simplification

The difficult part is of course to show that simplification observes the above equivalence. To begin with, it is easy to prove that

Proposition 4.2.11 M ≡ M′ implies CRes(M) ≡ CRes(M′).

We can apply this equivalence to our problem in some cases. For example,if we only transform the set of marked clauses equivalently: With M = \overline{α}(M) ∪ α(M) and M′ = \overline{α}(M′) ∪ α(M′), and assuming that \overline{α}(M) = \overline{α′}(M′) and α(M) ≡ \overline{α′}(M′), we have essentially substituted with an equivalent, and it is clear that Xα(M) ≡ Xα′(M′).

However, if we only know M ≡ M′, we have to think of a different approach. In the following, we will examine the equivalence preserving transformation that removes subsumed clauses from a set, and sketch how this can be extended to the case of removing implied clauses.

So assume that we have two clauses C_{1} ∈ \overline{α}(M), C_{2} ∈ α(M), C_{1} ⊴ C_{2} . We transform M into M′ = \overline{α}(M) ∪ α(M) \ C by removing C_{2}, and want to show (the marking function α is the same for both sets)

X(M) ≡ X(M′).

A crucial lemma is

Lemma 4.2.1 If C_{1} ⊴ C_{2} , then CRes(C_{1}) ⊴ CRes(C_{2}).

Proof. Special case of 4.2.2. □

Hence, if we guarantee that X(M′) contains (or implies) all C-resolvents of C_{1}, then all C-resolvents of C_{2} are also implied. However, if we delete C_{2}, we might loose some of the C-resolvents of C_{1}, for example, if C_{2} has been derived from C_{1}. To study this problem more closely, we will first visualize a state of the deduction process as a directed graph as in figure 4.4. Nodes of the graph represent clauses, and edges (C_{1}, C_{2}) represent the inference relation C_{1} = CRes(C_{2}). The additional arrows labeled A and B represent subsumptions. The figure depicts the following situation:

Figure 4.4: Visualization of a deduction state

We assume that we have for some time added resolvents and removed marks, but not done any simplifications. Note that no two equal clauses have been generated, which would have triggered subsumption simplification. Then the graph we defined is a set of trees, and all marked clauses are the leaves of the trees, since all inner nodes have descendants and therefore lost their marks. The roots of the trees represent the members R_{i} of the initial clause set M_{0} =^{def} ⋃_{i=1}^{n} R_{i}, and its closure CRes(M_{0}) can be evidently

be computed by computing their closures separately:

CRes(M_{0}) = ⋃_{i=1}^{n} CRes(R_{i}).

Denoting the ancestors and descendant of a clause C by Anc(C) and Dc(C), respectively, the figure should provide the intuition for CRes(R_{i}) =

X(Dc(R_{i})), and therefore with M = ⋃_{i=1}^{n} R_{i}, CRes(M_{0}) = X(M).

Now we can compare the subsumptions represented by the arrows A and B. The subsumption that arrow A visualizes literally cuts the branch on which our argumentation sits: the subsumed clause is marked, and therefore maybe necessary for generating resolvents, especially of the subsuming clause.

The case of C_{1} and C_{2} in the figure is different. The C-resolvents of both clauses can be computed independently, and the lemma 4.2.1 above can be applied. Let

R_{r} = ⋃_{i=3}^{n} R_{i},

and note that, for any sets M, N, CRes(M ∪ N) = CRes(M) ∪ CRes(N). With the latter, and since C_{2} is marked, we obtain from the definition of X that

X(R_{2}) = X(Dc(R_{2}) \ C_{2}) ∪ CRes(C_{2}).  (4.1)

The lemma yields, together with CRes(C_{1}) ⊆ CRes(R_{1}) ⊆ X(Dc(R_{1})),

X(Dc(R_{1})) ⊴ CRes(C_{2})  (4.2)

which we can use in

X(M) = CRes(M_{0})
= CRes(R_{1}) ∪ CRes(R_{2}) ∪ CRes(R_{r})
= X(Dc(R_{1})) ∪ X(Dc(R_{2})) ∪ X(Dc(R_{r}))
= X(Dc(R_{1})) ∪ X(Dc(R_{2}) \ C_{2}) ∪ CRes(C_{2}) ∪ X(Dc(R_{r}))
≡ X(Dc(R_{1})) ∪ X(Dc(R_{2}) \ C_{2}) ∪ X(Dc(R_{r})) by 4.2
= X(M′) by definition of M′

This proves our claim. Note that, as long as we have trees, we can define roots as above, and the argument is no longer limited to the assertion that all clauses in the input clause set still exists, which may not be true when using, for example, back subsumption.

The argument may be generalized. It is not necessary that C_{1}, C_{2} have different root nodes. It suffices that C_{2} is not a descendant of C_{1}. This criterion can be generalized to the case of extended subsumption, where S ⊧ C_{2} for some set of clauses S. Then we require that C_{2} is not among the descendants of any clause in S. Of course, for a similar argument, we need a parallel to lemma 4.2.1. This is given by

Lemma 4.2.2 If M ⊧ C, then CRes(M) ⊴ CRes(C).

Proof. (Sketch) We prove this using the resolution calculus. A well-known property of this calculus is that if M ⊧ C, then we can deduce some C′ subsuming C. We prove by induction that

CRes^{i}(pure, M) ⊢ CRes^{i}(pure, C′),

that is, the i-th layer of C-resolvents of C can be deduced from the i-th layer of C-resolvents. The closure CRes(M) then implies the closure CRes(C′), which by lemma 4.2.1 then subsumes CRes(C). □

However, the subsuming clauses are now “supporting” the subsumed clause in the sense that their closure must be computed in order to compute the closure of the subsumed clause (strictly speaking, this may not be necessary, but it is necessary for the line of argumentation given above to work). Further simplification rules must care not to delete supporting clauses without replacing them with another supporting clause. As long as all simplification rules respect the support structure, the above argumentation works. The critical case is when a clause is used to subsume a clause set by which it is supported. If we picture the support dependencies in a clause graph with added arrows for support relations, then one critical case are cycles, which occur when a clause can be used to simplify the set it is supported by.

With this method, we can only prove the correctness of XScan in its current form if we can prove that these cycles do not destroy it. In the case of simple subsumption, this presents no problem, while it seems more complicated in the case of extended subsumption. Yet, we have only treated the problem on a very abstract level, leaving aside a lot of information. For example, on the semantical side, we only use first-order equivalence arguments, though we have existentially quantified predicates. Additionally, on the syntactical side, we can examine where the existentially quantified predicates occur, and what role they play, for example, in a proof used by the extended subsumption rule. Hence, we believe it is justified to conjecture that XScan is correct in its current form.

One further note on the proof method. We think that a proof based on the above method will be technically complicated. There could be a lot of support from the theory of connection graph resolution (e.g. [Kow75]), which may also yield additional simplification rules. By its compact representation of potentially infinite resolution branches, it may provide a suitable theoretical means for reasoning about our problems. However, I see no way of entirely getting rid of syntactic arguments as long as the purity deletion criterion has a syntactic form.

4.2.7 Future work

Loops are a natural main issue in research on Scan. One direction of research might focus on patterns in clause sets generated by loops. With fixpoint methods as used in [NS95], these infinite sets can then reduced to finite ones.

Another direction of research should explore how loops can be avoided by clever combination of inference rules and inference strategies. A point of interest is whether simplification rules merely make the clause set smaller, or really avoid loops. For example, a subsuming clause in many cases can have infinitely many resolvents when the subsumed clauses has, and nothing maybe won. And of course loops may also be terminated by introducing redundancy instead of removing it.

Scan may prove a useful tool for studying second-order logic with quantifiers ranging over all functions from a deductive point of view. Furthermore, the close resemblance of the C-resolution rule and ordinary resolution gives rise to many speculations. For example, one might speculate that any complete calculus for some logic, especially modal logics, might be extended to a complete quantifier elimination algorithm for this logic (in the sense in that Scan is complete, that is, equivalent clause sets are enumerated). This offers a different view on completeness proofs for first-order logic and other logics. Maybe there are “lowering” techniques similar to the well-known lifting technique. Also, a study of the relation between both resolution rules may gradually abstract from their syntactical form, and hence lead to a deeper and more semantical understanding of their properties.

Although most of these points are already of interest in first-order logic, they now have a much wider applicability.

Unskolemize: Elimination of existentially quantified functions

In the last chapter, we presented Scan as an algorithm for eliminating existentially quantified predicate symbols from second-order formulas. Scan works on clauses and therefore eliminates first-order existential quantifiers by skolemization. The introduced skolem functions may still occur in Scan’s output, so their elimination poses a new quantifier elimination problem, which we will discuss in this chapter and tackle with the algorithm Unskolemize.

We will show that skolemization may be understood as a transformation of first-order existential quantifiers into second-order existential quantifiers. By reversing this transformation, second-order quantification over functions can be reduced to first-order quantification over individuals. The reversal of skolemization is a much less general approach to function elimination than the Scan approach is to predicate elimination. However, contrary to Scan, the Unskolemize algorithm, which is based on this approach, always terminates. Our algorithm improves an existing algorithm by McCune ([McC88]) in both scope and time complexity.

5.1 The problem of skolem functions in Scan

Consider the simple Scan output

P (x, f(x))

5.2. REVERSING SKOLEMIZATION AS FUNCTION ELIMINATION49

that contains the skolem function f before f is eliminated. We already remarked in chapter 4 that this must be interpreted as the second-order formula

∃f∀x P (x, f(x)).

Therefore, Scan has rather transformed a predicate elimination problem into a function elimination problem than solved a reduction problem. Consequently, we should feed back the new problem of eliminating f to Scan by coding f as a predicate F with functional properties. That is, we exploit

∃f∀x P (x, f(x))
≡  ∃f[∀x, y (P (x, y) ∨ y ≠ f(x))]
≡ ∃F [∀x, y (P (x, y) ∨ ¬F (x, y)) ∧ ∀x∃zF (x, z)]

with F (x, y) true iff f(x) = y. For F to be a function, we should have required that exactly one x for each x with F (x, y) exists, but for the syntactical issue we are up to, this is not relevant. When we input this formula to Scan, it is put into clause normal form and skolemized yielding two clauses:

C_{1} P (x, y) ∨ ¬F (x, y)

C_{2} F (x, f(x))

with a new skolem function f. Scan resolves C_{1} with C_{2} on F, which puts f back into the place where it annoyed us:

C_{3} : P (x, y) ∨ y ≠ f(x) ≡ P (x, f(x)).

It is clear that this approach fails in general, too. We now sketch an alternative approach, which is described in more detail in the subsequent sections.

5.2 Reversing skolemization as function elimination

Skolemization may be seen as a transformation of a first-order formula into a second-order one, by applying the following equivalence (see, for example, [vB83]) from right to left:

∀x̄∃yΦ[x̄, y] ≡ ∃f∀x̄Φ[x̄, y ↦ f(x̄)]  (5.1)

50CHAPTER 5. UNSKOLEMIZE: ELIMINATION OF EXISTENTIALLY QUANTIFIED FUNCTIONS

where x̄, y are free in Φ, and f does not occur in Φ[x̄, y].

For skolemization of a first-order formula, all existential quantifiers are eliminated by repeated application of this rewrite rule. If we skolemize a formula in prenex form, then the argument sets of the introduced skolem functions are linearly ordered by set inclusion, which can easily be seen.

Now we apply 5.1 in the other direction to eliminate f, as in the example above. Therefore, following McCune ([McC88]), we also call the elimination of existentially quantified functions unskolemization. We will now examine the conditions that allow us to unskolemize a formula with several skolem functions.

We assume the formula to be in the form of Scan output, that is, it is a clause set M = {C_{1}, C_{2}, …, C_{n}}, interpreted as the formula

∃f̄∀x̄ C_{1} ∧ C_{2} … ∧ C_{n}

where the C_{i} are clauses, and f̄, x̄ contain all skolem functions and free variables in M.

Note that a clause set M to be unskolemized must be in the form M′[y ↦ f(x̄)] for some clause set M′, that is, terms and subterms in M with the top symbol f must have the same argument lists, and they must only consist of variables. We say that f is required to be consistent in M. We say that M is consistent if all skolem functions in M are consistent.

In addition, we noted that in a skolemized prenex formula, all argument sets of skolem functions are linearly ordered by set inclusion. If a clause set satisfies this condition, we say that it is globally linear, or short linear.

Putting this together, we can unskolemize a clause set if it is both linear and consistent. In the following, we try to establish these conditions in a clause set by equivalence preserving transformations. The transformations we employ are

• variable abstraction and

• variable renaming in clauses.

Variable renaming is a well-known equivalence preserving operation on clauses:

Definition 5.2.1 (Renaming) A substitution σ is a (variable) renaming for a clause C if the restriction of σ on the variables of C is injective, that is

∀x, y ∈ V ars(C), x ≠ y implies σ(x) ≠ σ(y).

σ is a renaming for a set M of clauses if it is a renaming for each clause.

Variable abstraction is the replacement of terms by variables similar to the constraint elimination introduced in chapter 4. E.g., we use equivalences like

∀x P (f(a)) ∨ Q(g(x, a)) ≡ ∀x, y P (f(y)) ∨ Q(g(x, y)) ∨ y ≠ a.

Example 5.2.2 To illustrate the whole unskolemization process, consider the clauses

C_{1}: P (a, f(a)) ∨ Q(g(a, y))

C_{2}: R(f(b)) ∨ Q(g(b, w))

with the skolem functions f and g. By variable abstraction, we obtain

C_{1}: P (x, f(x)) ∨ Q(g(x, y)) ∨ x ≠ a

C_{2}: R(f(v)) ∨ Q(g(v, w)) ∨ v ≠ b.

and by renaming v to x and w to y, we have

C_{1}: P (x, f(x)) ∨ Q(g(x, y)) ∨ x ≠ a

C_{2}: R(f(x)) ∨ Q(g(x, y)) ∨ x ≠ b.

The conditions of consistency and linearity are met, so we can rewrite the formula corresponding to the clause set in two steps using 5.1, by introducing the first-order individual variables z_{g} for g and z_{f} for f.

∃f (∃g∀x, y P (x, f(x)) ∨ Q(g(x, y)) ∨ x ≠ a ∧
R(f(x)) ∨ Q(g(x, y)) ∨ x ≠ b)
≡ ∃f ∀x (∀y∃z_{g} P (x, f(x)) ∨ Q(z_{g}) ∨ x ≠ a ∧
R(f(x)) ∨ Q(z_{g}) ∨ x ≠ b)
≡ ∀x∃z_{f} (∀y∃z_{g} P (x, z_{f}) ∨ Q(z_{g}) ∨ x ≠ a ∧
R(z_{f}) ∨ Q(z_{g}) ∨ x ≠ b)

Note that we have to start the quantifier prefix conversion with the function having the most arguments if we want to apply 5.1 successively.

By SkExpr(M), SkExpr(C), SkExpr(t), we denote the set of skolem expressions occurring in a clause set M, clause C or term t. ∥t∥ for a term t = f(s̄) denotes, a little sloppy, the arity of the top symbol f of t. We now give exact algorithms for performing the steps sketched above.

5.2.1 Normalizing argument lists by variable abstraction

Proposition 5.2.3 Let C be a clause, z ∉ V ars(C) a fresh variable not occurring in C. Let Π = {π_{1}, …, π_{n}} be a set of occurrences of the term t in C, that is, C|_{π_{i}} = t. Then

∀x̄ C ≡ ∀x̄, z C[Π/z] ∨ z ≠ t

where x̄ contains the free variables in C.

For example, we have

P (a, a) ≡ ∀x P (x, a) ∨ x ≠ a.

Using this equivalence repeatedly on all arguments of skolem functions, we can assure that all skolem expressions only have variable arguments. Note that the above proposition does not force us to replace a term t everywhere in the clause when we abstract it, as shown in the example. This will be exploited in the next section.

We call expressions with only variable arguments flat. The algorithm Abstract flattens all skolem functions in a clause. For brevity, by f[t] we denote a function f with a non-variable term t as one of its arguments, and by C[f] a clause C containing the function symbol f. C[t ↦ z_{t}] denotes the clause that results from replacing t in C by z_{t}.

Algorithm 5.2.4

set<clause> Abstract( set<clause> M) While (There is a clause C[f] ∈ M containing a non-linear skolem expression f[t]){

Let C′ = C[t ↦ z_{t}] ∨ z_{t} ≠ t; // z_{t} does not occur in C

Let M = (M ∪ C′) \ C; }
Return(M);

5.2.2 Establishing argument uniqueness

Given a clause set M with only flat skolem functions, we can use proposition 5.2.3 again to ensure that each variable argument of each skolem function occurs only once in the argument list. Then we say that M satisfies the condition of uniqueness. For example, we replace

P (x, f(x, x)) ∨ Q(g(x, y, y))

by

P (x, f(x, z)) ∨ Q(g(x, v, y)) ∨ z ≠ x ∨ v ≠ y.

For the algorithm Unskolemize, we choose the abstractions establishing argument uniqueness in such a way that the consistency and linearity of a clause is preserved, i.e., skolem expressions headed by the same skolem function symbol are already equal, and the argument sets of all skolem expressions are linearly ordered by set inclusion.

Unfortunately, sometimes it is impossible to preserve these properties when uniqueness of arguments is required. For example, consider the unit clause

P (f(x, x), g(x, y)),

where f, g are skolem functions. It is obvious that there cannot be a unique abstraction that established argument uniqueness and preserves local linearity. However, if the argument lists are ordered by multiset inclusion, then the following (straightforward) algorithm Unique preserves this order. It assumes that all skolem expressions in the input clause set are flat. Algorithm 5.2.5

set<clause> Unique( set<clause> M)

// While there is a skolem expression with duplicate arguments in M While (∃C ∈ M, π_{f} ∈ Occ(C) such that C|_{π_{f}} = f(x̄) ∈ SkExpr(C)

and |Occ(f(x̄), w)| ≥ 2 for some variable w){ // Replace one (any) occurrence of w in every skolem expression // in C that contains w more than once // Collect these expressions in Dup Let Dup = {π_{i} | |Occ(C|_{π_{i}}, w)| ≥ 2} For (i = 1 To |Dup|) Let s = C|_{π_{i}}; Choose ρ_{i} ∈ Occ(s, w);

// Replace all occurrences with a fresh variable u ∉ V ars(c)

Let C′ = C[ρ_{i}, …, ρ_{|Dup|}/u];

Let C′ = C′ ∨ u ≠ w; Let M = M \ C ∪ {C′}; }

Return(M);

It is easy to see that Unique preserves equivalence of a clause set:

Lemma 5.2.1 For a clause set M with skolem expressions occurring only flat,

∃f̄∀x̄M ≡ ∃f̄∀x̄ Unique(M)

Proof. In the algorithm, we have C ≡ C′ by 5.2.3, so in M clauses are only substituted by equivalent ones, which preserves equivalence. □

The algorithm Unique makes arguments unique preserves strong linearity in a clause, which we will define by

Definition 5.2.6 (Strong local linearity) Let C be a clause. Let f(s̄) and g(t̄) be two skolem expressions occurring C. If for any such two expressions, ∥f∥ ≤ ∥g∥, then

|Occ(f(s̄), s_{i})| ≤ |Occ(g(t̄), s_{i})|.

That is, the argument sets of f and g are linearly ordered by set inclusion, and each argument of f occurs in g at least as often as in f. In other words, they are linearly ordered by multiset inclusion.

We say that a clause set M is strongly locally linear if all its clauses are.

Proposition 5.2.7 Let M be a clause set with all skolem expressions flat. If M is strongly locally linear, then Unique(M) is.

Proof. The proof needs no special ideas, but requires some formal care. We have to show that Unique(M) is strongly locally linear. We examine the step that constructs C′ from C and show that C′ as in the definition of Unique is strongly locally linear if C is.

To begin with, we define red(s, w, u) as the result of replacing one occurrence of the variable w in the flat skolem expression f by the variable u, if w occurs more that once in the argument list of s, and s otherwise. We will use red to analyze the abstraction step in the Unique algorithm.It is easy to see that

(1) Args(s) ⊆ Args(red(s, w, u))

for any s, w, u with u ∉ Args(s). Furthermore, for two flat skolem expressions s_{f}, s_{g} with Args(s_{f}) ⊆ Args(s_{g}), and any variable u ∉ Args(s_{f}) ∪ Args(s_{g}) we have

(2) ∀v |Occ(s_{f}, v)| ≤ |Occ(s_{g}, v)| implies ∀w red(s_{f}, w, u) ⊆ red(s_{g}, w, u),

which can easily be shown using (1) and examining the cases w ∈ Args(f) and w ∉ Args(f).

Now we look at the abstraction step in Unique. Let w and u denote the same variables as in the algorithm. By assumption, C is strongly locally linear. Consider two occurrences π_{f}, π_{g} ∈ Occ(C′) of skolem expressions with C′|_{π_{f}} = s′_{f}, C′|_{π_{g}} = s′_{g}. By the definition of C′, it is easy to see that

π_{f}, π_{g} ∈ Occ(C). Let s_{f} =^{def} C|_{π_{f}} , s_{g} =^{def} C|_{π_{g}}. Again by the definition of C′ and red, we have

(3) s′_{f} = red(s_{f}, w, u) and s′_{g} = red(s_{g}, w, u).

Then, we also have ∥s_{f}∥ = ∥s′_{f}∥ and ∥s_{g}∥ = ∥s′_{g}∥ because the functions symbols are unchanged by red, which implies ∥s_{f}∥ ≤ ∥s_{g}∥, and therefore, exploiting that C is strongly locally linear,

s_{f} ⊆ s_{g} and |Occ(s_{f}, v)| ≤ |Occ(s_{g}, v)| for any variable v,

so s_{f} and s_{g} satisfy the preconditions of (2). With (3), we can substitute red(s_{f}, w, u) by s′_{f} and red(s_{g}, w, u) by s′_{g} in (3), resulting in

s′_{f} ⊆ s′_{g} and |Occ(s′_{f}, v)| ≤ |Occ(s′_{g}, v)| for any variable v.

which was to be proven. □

5.2.3 Establishing consistency

The next algorithm Consistency establishes consistency of skolem expressions in a clause set M with only flat skolem expressions by computing an appropriate substitution σ. We call σ a globally consistent substitution, or short, consistent substitution. If a consistent substitution for M exists, Consistency finds one. This substitution has several important properties:

• If there is some μ such that μ(M) is globally consistent, then σ(M) is globally consistent.

• If there is some consistent μ that is also a renaming of M, then Consistency finds some such σ. We call μ a consistent renaming.

• If M satisfies uniqueness of arguments, and there is a consistent renaming μ of M such that μ(M) satisfies uniqueness of arguments, then σ(M) does.

We need

Definition 5.2.8 (Local and global consistency) A skolem function f is consistent in a clause C if all skolem expressions headed by f in C are equal. It is consistent in a clause set M if all skolem expressions headed by f in M are equal.

A clause C is consistent, if all skolem functions are consistent in it. A clause set M is locally consistent if all its clauses are consistent. A clause set M is globally consistent if all skolem functions are consistent in it.

If a clause is not consistent, then there is no renaming that can make it consistent, which can easily be seen, so the algorithm assumes a locally consistent input clause set M. The idea behind the algorithm is to collect variables in sets that must necessarily be mapped on the same variable by any consistent renaming, and then construct a substitution from these sets. Extending our previous definition, we define SkExpr(M, f) to be the set of all skolem expressions in a clause set M headed by the skolem function symbol f. We will need to “flatten” a set of sets:

F lat({M_{1}, …, M_{n}}) =^{def} ⋃_{i=1}^{n} M_{i}.

Now for the algorithm. Its input consists of a clause set M and an empty substitution σ by reference, and it alters σ such that σ(M) is consistent. It returns σ(M) and the substitution by reference. See figure 5.1 for the algorithm. We give an example.

Example 5.2.10 For Consistency, only the skolem functions in a clause matter, which is why we consider only sets of skolem functions representing clauses in the following. Consider the skolem function sets

\begin{matrix}C_{1} : & \{f(x_{1}), g(x_{1}, x_{2})\} \\ C_{2} : & \{g(y_{2}, y_{3}), h(y_{1}, y_{2}, y_{3})\} \\ C_{3} : & \{f(z_{1}), h(z_{1}, x_{2}, z_{3})\} \end{matrix}

Consistency computes the set E^{0}

\{ \begin{matrix}\{\{x_{1}, z_{1}\}_{f_{1}}\}, \{\{x_{1}, y_{2}\}_{g_{1}}\}, \{\{x_{2}, y_{3}\}_{g_{2}}\} \\ \{\{y_{1}, z_{1}\}_{h_{1}}\}, \{\{y_{2}, z_{2}\}_{h_{2}}\}, \{\{y_{3}, z_{3}\}_{h_{3}}\} \end{matrix} \}

where sets are indexed with the function and the argument position of the function whose consistency condition they represent. Now Consistency Algorithm 5.2.9

set<clause> Consistency( set<clause> M, substitution &σ) Let E^{0} = ∅; Foreach (Skolem function f)

// Collect the i-th arguments of each expression For i = 1 To ∥f∥ Do {

Let A = {x | ∃s ∈ SkExpr(M, f) with x = s|_{i}}; Let E^{0} = E^{0} ∪ {{A}}; }

// Now join sets in E as long as their flattenings are not all disjoint Let j = 0; While (∃E_{1}, E_{2} ∈ E^{j} with F lat(E_{1}) ∩ F lat(E_{2}) ≠ ∅){

Let E^{j+1} = E^{j} \ {E_{1}, E_{2}} ∪ {E_{1} ∪ E_{2}};

Let j = j + 1; }

// Now build substitution σ. // Assume u_{i} ∉ M to be a fresh variable // for 1 ≤ i ≤ |E^{j}|, and let // E^{j} = {E_{1}^{j}, …, E_{|E^{j}|}^{j}} Let σ = ∅; For i = 1 To |E^{j}|

Let σ = σ ∪ ⋃_{v∈F lat(E_{i}^{j})}{v ↦ u_{i}}; Let M′ = σM; Return(M′);

Figure 5.1: The algorithm Consistency successively puts sets with common variables in one set:

\{ \begin{matrix}\{\{x_{1}, z_{1}\}_{f_{1}}\}, \{x_{1}, y_{2}\}_{g_{1}}\}, \{\{x_{2}, y_{3}\}_{g_{2}}\} \\ \{\{y_{1}, z_{1}\}_{h_{1}}\}, \{\{y_{2}, z_{2}\}_{h_{2}}\}, \{\{y_{3}, z_{3}\}_{h_{3}}\} \end{matrix} \} since g_{1} ∩ f_{1} = \{x_{1}\}

\{ \begin{matrix}\{\{x_{1}, z_{1}\}_{f_{1}}, \{x_{1}, y_{2}\}_{g_{1}}, \{y_{2}, z_{2}\}_{h_{2}}\}\}\} \\ \{\{x_{2}, y_{3}\}_{g_{2}}, \{y_{1}, z_{1}\}_{h_{1}}\}, \{\{y_{3}, z_{3}\}_{h_{3}}\} \end{matrix} \} since h_{2} ∩ g_{1} = \{y_{2}\}

\{ \begin{matrix}\{\{x_{1}, z_{1}\}_{f_{1}}, \{x_{1}, y_{2}\}_{g_{1}}, \{y_{2}, z_{2}\}_{h_{2}}\}\} \\ \{\{x_{2}, y_{3}\}_{g_{2}}, \{y_{3}, z_{3}\}_{h_{3}}\}, \{\{y_{1}, z_{1}\}_{h_{1}}\} \end{matrix} \} since h_{3} ∩ g_{2} = \{y_{3}\}.

Now all flattenings of “variable set”-sets are disjoint. The variables in these sets are now assigned new variables, yielding the substitution (abbreviated)

σ{{x_{1}, z_{1}, y_{2}, z_{2}} ↦ u_{1}, {y_{3}, z_{3}, x_{2}} ↦ u_{2}, {y_{1}, z_{1}} ↦ u_{3}}.

Applying σ to the function set, we get

\begin{matrix}σ(C_{1}) : & \{f(u_{1}), g(u_{1}, u_{2})\} \\ σ(C_{2}) : & \{g(u_{1}, u_{2}), h(u_{3}, u_{1}, u_{2})\} \\ σ(C_{1}) : & \{f(u_{1}), h(u_{3}, u_{1}, u_{2})\}. \end{matrix}

σ obviously is a consistent renaming.

Now for the properties of Consistency. It is clear that it always terminates, as E^{0} is finite and |E^{j+1}| ≤ |E^{j}|. We show that the algorithm is correct and complete, starting with correctness.

Proposition 5.2.11 For any locally consistent clause set M, Consistency(M) is a globally consistent clause set.

Proof. We have to check that σ is a substitution, that is, no variable is “mapped” on two different variables. This is so because F lat(E_{1}) ∩ F lat(E_{2}) = ∅ for all E_{1}, E_{2} ∈ E^{j} at the end of the algorithm.

σ also makes M globally consistent. If, for a skolem function f, |SkExpr(M, f)| = 1, then it already is consistent, and any substitution preserves its consistency.

If |SkExpr(M, f)| ≥ 2, then consider any two argument variables v_{1}, v_{2} in the same argument position of two different skolem expressions f(x̄_{1}), f(x̄_{2}), both headed by f. Then there is some E ∈ E^{0} such that v_{1}, v_{2} ∈ F lat(E), by definition of E^{0}. But then, by definition of the E^{j}, there is some E_{j} ∈ E^{j} such that E ∈ E^{j}, so both variables are assigned the same value at the end of the algorithm. This is easily proven by induction over j. □

We specified several completeness conditions for Consistency at the beginning of the section and now prove them. They all follow from a minimality condition that the algorithm satisfies and which says that Consistency identifies variables only if they have to be identified by any consistent substitution.

Lemma 5.2.2 Let σ be the substitution computed by Consistency. Let σ(v) = σ(w) for some two variables in M. If there is a consistent substitution μ for M, then μ(v) = μ(w).

Proof. We show by induction over k that every consistent substitution μ must map all variables of the set F lat(E^{k}), E^{k} ∈ E^{k} on the same variable. For k = 0, this is clear by definition of E^{0} and the definition of consistency.

Now assume this is true for some k ≤ n, where n is the value of the variable j at the end of the algorithm. As in the algorithm, let E_{1}, E_{2} ∈ E^{k}, F lat(E_{1}) ∩ F lat(E_{2}) ≠ ∅ be given, which exist because otherwise the algorithm would have terminated before. We have to prove the induction hypothesis for all E ∈ E^{k+1}. Consider some E ∈ E^{k+1}. If E ∈ E^{k}, then our claim is true because of the induction hypothesis. If E ∉ E^{k}, then E = E_{1} ∪ E_{2}, so there is some variable v ∈ F lat(E_{1}) ∩ F lat(E_{2}). Now, by the induction hypothesis, for all variables in F lat(E_{i}), i ∈ {1, 2}, are mapped on the same variable, that is, for all w ∈ F lat(E_{i}), i ∈ {1, 2}, μ(v) = μ(w), so we have μ(v) = μ(w) also for all w ∈ F lat(E_{1}) ∪ F lat(E_{2}). This completes the proof. □ Now the completeness conditions follow easily.

Proposition 5.2.12 Let σ be the substitution computed by Consistency for a clause set M. If there is some consistent renaming μ of M, then σ is a consistent renaming. If there is a consistent renaming μ of M that preserves uniqueness of arguments, then σ does also.

Proof. We prove by contradiction. Assume that σ is not a consistent renaming, though there exists one. Then for some clause C and for some variables x, y ∈ V ars(C), x ≠ y,σ(x) = σ(y). By 5.2.2, then μ(x) = μ(y), which contradicts the assumption that μ is a renaming. Preservation of argument uniqueness is proven analogously. □

5.2.4 Establishing linearity

Finally, we must find a renaming a consistent clause set M which puts all argument sets of skolem expressions in M into a linear order. We then say that M is globally linear and define two related useful notions:

Definition 5.2.13 (Local and global linearity) We say that a clause is linear, if the argument list of its skolem expressions are linearly ordered by set inclusion, that is, for some skolem expressions s_{1}, s_{2} in C,

Args(s_{1}) ⊆ Args(s_{2}) or Args(s_{2}) ⊆ Args(s_{1}).

We say that a clause set M is locally linear if all its clauses are linear. We say that M is globally linear if the argument list of all its skolem expressions are linearly ordered by set inclusion.

It is easy to see that a non-linear clause cannot be made linear by any renaming, so we require local linearity (LL) of M for the next algorithm Linearity, which we abbreviate by (LL). Also, we require M to satisfy uniqueness of argument lists (U), consistency (C) and minimal consistency (MC) as formulated in 5.2.2.

To start with, we give a criterion that is necessary and sufficient for the existence of a globally linear renaming of a consistent clause set, that is, a renaming ρ such that ρ(M) is globally linear. For two sets M_{1}, M_{2}, we write M_{1} ⊆⊇ M_{2} if M_{1} ⊆ M_{2} or M_{2} ⊆ M_{1}.

Proposition 5.2.14 (Extendible linearity) If a clause set M fulfills (C), (U), (LL) and (MC), there exists a consistent globally linear renaming ρ of M if and only if for any skolem expressions s_{1}, s_{2}, s_{3}, we have

Args(s_{1}), Args(s_{2}) ⊆ Args(s_{3}) implies Args(s_{1}) ⊆⊇ Args(s_{2}),

that is, set inclusion orders {Args(s_{1}), Args(s_{2}), Args(s_{3})} linearly.

We first prove necessity of this criterion (EL). For sufficiency, we afterwards prove an intermediate lemma, and then give an algorithm that computes ρ as desired if (EL) is fulfilled.

Lemma 5.2.3 (Necessity of (EL)) If there is some renaming ρ making M globally linear, then (EL) holds for M.

Proof. We show by contraposition that (EL) must hold since otherwise a substitution making M globally linear could not be a renaming.

Now assume that ρ(M) is globally linear, and that s_{1}, s_{2}, s_{3} exist such that Args(s_{1}), Args(s_{2}) ⊆ Args(s_{3}), but Args(s_{1}) ⊆⊇ Args(s_{2}) is violated, so that there exists some variable v ∈ Args(s_{1}) with v ∉ Args(s_{2}). W.l.o.g., we assume that Args(s_{1}) ⊆ Args(s_{2}).

We begin by showing that

(∗) Args(ρ(s_{1})) ⊆ Args(ρ(s_{2})).

Since ρ is a renaming, it is a bijection on the argument lists of the s_{i}, which implies |Args(s_{i})| = |ρ(Args(s_{i}))| for i ∈ {1, 2, 3}. Now if |Args(s_{1})| = |Args(s_{2})|, then

(∗∗) |Args(ρ(s_{1}))| = |Args(ρ(s_{2}))|.

ρ(M) is globally linear, therefore Args(ρ(s_{1})) ⊆⊇ Args(ρ(s_{2})). With (∗∗), this even implies Args(ρ(s_{1})) = Args(ρ(s_{2})).

If |Args(s_{1})| < |Args(s_{2})|, then

(∗∗) |Args(ρ(s_{1}))| < |Args(ρ(s_{2}))|.

But then Args(ρ(s_{2})) ⊆ Args(ρ(s_{1})) is of course impossible, which with Args(ρ(s_{1})) ⊆⊇ Args(ρ(s_{2})) implies (∗).

Now, since (∗) holds, with v as above, there is some x ∈ Args(s_{2}), x ≠ v such that ρ(v) = ρ(x). But Args(s_{1}), Args( s_{2}) ⊆ Args(s_{3}), so x, v ∈ Args(s_{3}), that is ρ identifies two variables in the same expression, hence it cannot be a renaming as was assumed. □ The next lemma allows us to abstract from the clause structure and to operate on variable sets only.

Lemma 5.2.4 If (EL) and (MC) hold for M, then for any two skolem expressions s_{1}, s_{2} with Args(s_{1})∩Args(s_{2}) ≠ ∅ there exists a skolem expression s_{3} in M such that Args(s_{1}) ∩ Args(s_{2}) = Args(s_{3}).

Proof. (Sketch) To prove this, we need the notion of dominance, which is defined relatively to a clause set M which we take as constant in the following. A skolem function f directly dominates another function g if they both occur in the same clause, and Args(g) ⊆ Args(f). Note that dominance is reflexive. Domination is the transitive closure of direct domination. We write f ⪰ g if f dominates g. This notion is well-defined because of local linearity and consistency. For two skolem expressions s_{1} = f(x̄), s_{2} = g(ȳ), it is easy to see that with (MC) and (LL),

f ⪰ g implies Args(s_{2}) ⊇ Args(s_{1}).

Now for the proof. We distiguish three cases. If f and g are both dominated by some h, then by (EL) and the above, we have Args(f) ⊆⊇ Args(g), and the claim holds.

Now assume there is no such common dominating function. Then consider the sets D_{f} and D_{g} which contain the skolem expressions in M headed by functions dominated by f and g. By (EL), both sets are already linearly ordered by set inclusion on their arguments lists. Now D_{f} ∩ D_{g} is empty or not. If it is empty, define S = ∅. If it is not empty, take C to be D_{f} ∩ D_{g}, and s_{3} = h(z̄) to be the maximum function h with respect to set inclusion on argument sets, which is again well-defined by (EL) and consistency. We show that s_{3} is the searched function, if it exists, or that otherwise Args(s_{1}) ∩ Args(s_{2}) = ∅. In other words, we show that Args(s_{1}) ∩ Args(s_{2}) = S. Args(s_{1}) ∩ Args(s_{2}) ⊇ S is easy. For S = ∅, this is trival, and if S ≠ ∅, then this follows because both f and g dominate h. For the other direction Args(s_{1}) ∩ Args(s_{2}) ⊇ S, we assume that there is some v ∈ x̄ ∩ ȳ such that v ∉ z̄. We then change v in all clauses which contain functions that are dominated by some function that also dominates f to a new variable u not in M. This does not destroy consistency, and v is not changed in g. Essentially, this is so because in all clauses with functions dominated by g and f, v may change, but the common dominated functions do not contain v, and functions that dominate f or g only occur in different clauses by assumption (this step requires a little elaboration).

But then we found a consistent renaming with less variable identifications than before, which contradicts (MC). □ Now we define the algorithm Linearity, which operates only on terms.

Example 5.2.16 As in the example for the Consistency algorithm, we only consider the skolem function sets contained in clauses instead of the whole clauses. Let the following clause set be an output of Consistency:

C_{1} : {f(v_{1}), g(v_{1}, v_{2})}
C_{2} : {f(v_{1}), h(v_{1}, y_{1}, y_{2})}
C_{3} : {f(v_{1}), g(v_{1}, v_{2}), k(v_{1}, v_{2}, z)}

Linearity represents this by

A = {{v_{1}}, {v_{1}, v_{2}}, {v_{1}, y_{1}, y_{2}}, {v_{1}, v_{2}, z}}.

Then the σ_{j} are computed:

σ_{1} = {v_{1} ↦ u_{1}}
σ_{2} = σ_{1} ∪ {v_{2} ↦ u_{2}}
σ_{3} = σ_{2} ∪ {y_{1} ↦ u_{3}, y_{2} ↦ u_{2}}
σ_{4} = σ_{3} ∪ {z ↦ u_{3}}.

Algorithm 5.2.15

set<clause> Linearity( set<clause> M) // Collect all argument sets of skolem expressions in a set A Let S = SkExpr(M); Let A = ⋃_{s∈S}{Args(s)}; Let σ_{0} = ∅; // Build up substitution σ // Assume that S = {V_{1}, …, V_{n}} with |V_{j}| ≤ |V_{j+1}| // for 1 ≤ j ≤ n − 1 For j = 1 To n Do {

// Let {x_{1}, …, x_{l}} denote the variables in V_{j} // with σ(x_{i}) = x_{i} for 1 ≤ i ≤ l } // and let the u_{i} be fresh variables not in A Let σ_{j} = σ_{j−1} For i = 1 To l

Let σ_{j} = σ_{j} ∪ {x_{i} ↦ u_{|V |−i+1}}; } Return(σ_{n}(M));

Figure 5.2: The algorithm Linearity σ is a renaming, and, applied to the skolem functions, we have linearity:

σ(C_{1}) : {f(u_{1}), g(u_{1}, u_{2})}
σ(C_{2}) : {f(u_{1}), h(u_{1}, u_{3}, u_{2})}
σ(C_{3}) : {f(u_{1}), g(u_{1}, u_{2}), k(u_{1}, u_{2}, u_{3})}

We show that Linearity indeed computes a linear renaming if (EL) and (MC) hold for M, which is the case if M is the output of Consistency.

Lemma 5.2.5 σ_{n} as computed by Linearity(M) is a linear renaming if (MC) and (EL) hold for M.

Proof. It is easily shown by induction on j that σ(V_{j}) = {u_{1}, …, u_{|V_{j}|}},which gives linearity of σ.

To show that σ is a renaming, first note that be the definition of A and by lemma 5.2.4, which holds because (MC) holds, A is closed under intersection. We show that for any two distinct variables x, y occurring in some V_{j} ∈ A, we have σ_{i}(x) ≠ σ_{i}(y). Let V_{i_{x}}, V_{i_{y}} denote the sets that were processed when x and y were assigned one of the u_{i}. Now either V_{i_{x}} = V_{i_{y}} or not.

If V_{i_{x}} = V_{i_{y}}, then x and y were assigned one of the u_{i} at the same time, and different variables by definition of the algorithm.

Now assume V_{i_{x}} ≠ V_{i_{y}}.

If V_{i_{x}} is not a subset of V_{j}, then I =^{def} V_{j} ∩ V_{x} is a proper subset of V_{j}. As A is closed under intersection, I ∈ A. But x ∈ V_{j} by assumption, x ∈ V_{i_{x}} by definition, so that x ∈ V_{j} ∩ V_{i_{x}} = I with |I| ≤ |V_{i_{x}}| because I is a proper subset of V_{j}. But then x already occurred in a smaller set an must have been labeled before V_{i_{x}} was processed, which contradicts the choice of V_{i_{x}} .

Thus, it remains that V_{i_{x}} ⊂ V_{j}, and V_{y} ⊂ V_{j} by the same arguments, hence by (EL), V_{x} ⊆⊇ V_{y}.

W.l.o.g., V_{i_{x}} ⊆ V_{i_{y}}, so that x was assigned u_{k} with k ≤ |V_{i_{x}}|. Besides, all variables v ∈ V_{i_{x}} were already assigned new variables when V_{i_{y}} was processed, and y ∉ V_{i_{x}} by definition of V_{i_{y}}, so y was assigned some u_{l} with l > |V_{i_{x}}|. □

This proof completes the proof of proposition 5.2.14.

5.2.5 The basic Unskolemize algorithm

Now we integrate the algorithms of the previous sections in one algorithm Unskolemize. We prove it correct and make some observations about its completeness.

The algorithm Unskolemize, shown in figure 5.3, takes a second-order formula Φ = ∃f̄∀x̄ M as input, where M is a conjunction of clauses, and tries to reduce it to an equivalent first-order one. If it succeeds, it returns a formula without second-order quantifiers, if it fails, a second-order formula equivalent to the input. In any case, Unskolemize(Φ) ≡ Φ.

We assume that M, conceived as a set of clauses, cannot be partitioned into two clause sets M_{1}, M_{2}, such that the sets S_{1}, S_{2} of skolem functions in M_{1}, M_{2} are disjoint. If this were the case, we could unskolemize M_{1} and M_{2} clause sets separately, by the rules for quantifier distribution. We also

Algorithm 5.2.17

formula Unskolemize( formula ∃f̄∀x̄M)

Let M = Separate(M); Let M_{a} = Abstract(M); Let found = false; // signals solution Let A = {all abstractions α that make M unique} While (A ≠ ∅ and ¬found){ Choose α ∈ A; Let A = A \ {α}; // Apply abstraction (informal notation) Let M_{u} = α(M_{a}); Let σ = ∅; Let M_{c} = Consistency(M_{u}, &σ); If (σ is a global renaming and

M_{c} satisfies local and extendable linearity conditions) then{ Let M_{l} = Linearity(M_{c});

Let Φ = Reduce(∃f̄∀x̄M_{c});
Let found = true; }

// Return input if unskolemization failed If (¬found) Let Φ = ∃f̄∀x̄M; Return(Φ);

Figure 5.3: The algorithm Unskolemize

assume an algorithm Reduce which converts a consistent, globally linear clause set by equivalence 5.1 into an equivalent first-order formula. This algorithm consists of simply applying proposition 5.1 to the skolem symbols in order of decreasing arity, as we already demonstrated in the example 5.2.2. Finally, the algorithm Separate makes clauses in a clause set M pairwise variable disjoint.

Proposition 5.2.18 (Correctness of Unskolemize) For any formula ∃f̄∀x̄ M, where M is a disjunction of clauses,

Unskolemize(∃f̄∀x̄ M) ≡ ∃f̄∀x̄ M.

Proof. This follows from the properties of the used algorithms and transformations. Note that the preconditions for Linearity are satisfied: M_{u} is unique, and any renaming must preserve this property, so (U) is satisfied. (EL) and (LL) are demanded by the algorithm, and (MC) is guaranteed by the properties of Consistency. □

Note that a successful unskolemization may depend on the way arguments are made unique by Unique. Consider the unit clauses

P (g(x, x), f(x, x))
Q(g(y, y), f(y, y), a).

Two unique equivalent versions are

P (g(x, u), f(x, u)) ∨ x ≠ u
Q(g(y, v), f(y, v), a) ∨ v ≠ y.

and

P (g(x, u), f(u, x)) ∨ x ≠ u
Q(g(y, v), f(y, v), a) ∨ v ≠ y.

The first version can obviously be renamed consistently, while the second one can not: any consistent substitution σ would have to satisfy σ(x) = σ(y) and σ(u) = σ(y), therefore σ(x) = σ(u), so σ could not be a renaming. Hence, we may have to try all possibilities for making a clause set unique.

5.3 Extensions of Unskolemize

We now list two cases for which Unskolemize fails and propose ways of treating them in general.

5.3.1 Uniqueness revisited

We have already shown in 5.2.2 that sometimes uniqueness of arguments cannot be obtained without destroying local linearity. The example clause was

P (f(x, x), g(x, y)).

However, the following equivalence can help to make f unique without variable abstraction:

Proposition 5.3.1 Let ϕ(y) be a first − order formula with the free variable y, f a function not occurring in ϕ. Then

∃f ϕ(y ↦ f(x_{1}, …, x_{i}, …, x_{j}, …, x_{n})) ≡ ∃f ϕ(y ↦ f(x_{1}, …, x_{i}, …, x_{n}))

if x_{i} and x_{j} denote the same variable.

We could then replace the above clause by the equivalent (interpreted as second-order formula)

P (f(x), g(x, y)),

which is easily unskolemized by Unskolemize. In general, we can extend Unskolemize by a procedure that, for each skolem function, tries to make it consistent in the clause set, and then replaces it with a function without duplicate arguments.

5.3.2 Henkin quantifiers

Henkin quantifiers are a generalization of first-order quantifiers that may sometimes allow us to write second-order formulas we cannot unskolemize in a suggestive way. Consider the following clause:

P (x, y, f(x), g(y))

with the skolem functions f and g. As opposed to clauses obtained by skolemization, the argument sets of the skolem functions are not linearly ordered by set inclusion, and as they are in one clause, Unskolemize fails. Leon Henkin ([Hen61]) suggested to write the corresponding second-order formula ∃f, g ∀x, y P (x, y, f(x), g(y)) as

\binom{∀x∃z_{f}}{∀y∃z_{g}}P (x, y, z_{f}, z_{g})

to indicate that z_{f} only depends on x, and z_{g} only on y. We generalize this notation for our purposes to

( ∀x̄_{1}∃y_{1} ; ⋮ ; ∀x̄_{n}∃y_{n} ) ϕ(x̄_{1}, …, x̄_{n}, y_{1}, …, y_{n})

as an abbreviation for

∃f_{1}, …, f_{n} ∀x̄_{1}, …, x̄_{n} ϕ(y_{1} ↦ f_{1}(x̄_{1}), …, y_{n} ↦ f_{n}(x̄_{n})),

where the f_{i} do not occur in ϕ. The following proposition states that all clause sets can be unskolemized using Henkin quantifiers.

Proposition 5.3.2 Let M be a clause set with skolem functions, interpreted as the second order formula ∃f̄∀x̄ M. This formula can be equivalently be written with a Henkin quantifier in the above form.

Proof. We only have to prove that we can transform M into the form of ϕ above, that is, all skolem functions are renamed consistently. By the proposition 5.2.3 used for variable abstraction, we can rewrite all skolem functions in such a way that any two occurrences of skolem functions have disjoint argument sets, even within clauses, and all variables are unique in each argument list. It is obvious to see that M has a consistent renaming in this form, which was to be proven. □

5.4 The McCune algorithm

In [McC88], McCune describes an algorithm for eliminating skolem functions. It is only proven and designed to be satisfiability preserving, but can also be shown to be equivalence preserving. Though independently developed, it works in much the same way as Unskolemize: First tries to establish global consistency, then global linearity. Variable abstraction is employed to achieve consistency in practically the same way as in Unskolemize. Indeed, the consistent set M_{c} in the algorithm Unskolemize is the same set that is the input to the linearization phase of the McCune algorithm.

However, the linearization phase of McCune’s algorithm is much different. It has exponential time complexity and also fails to unskolemize some clause sets for which Unskolemize succeeds. Given a consistent clause set, 5.5. SOME REMARKS ON THE SCOPE AND COMPLEXITY OF UNSKOLEMIZE69

the algorithm attempts, for each permutation of all argument sets of skolem expressions, to unify all skolem expressions that are headed by functions of the same arity. Afterwards, it checks whether the computed unifier is a renaming. Of course, the number of permutations of each argument set grows exponentially with its size, and the number of combinations of the permutations of all arguments sets grows exponentially with the number of functions. Furthermore, this technique fails for simple clause sets. For example, consider the consistent clause set

P (f(x), g(x, y))
P (f(x), h(x, u, v))

All skolem expressions headed by functions with the same arity are already unified, but the clause set is not globally linear, hence it cannot be unskolemized. Unskolemize finds the obvious solution by unifying y and u.

5.5 Some remarks on the scope and complexity of Unskolemize

This section gathers some observations about the classes of formulas that Unskolemize can unskolemize and its time complexity.

5.5.1 Scope

We should at least expect Unskolemize to unskolemize all clause sets for which this is possible by renaming. However, we have already seen that this is not possible because Unique may destroy the local linearity of a clause, which makes it impossible to find a globally linear renaming. We conjecture that the algorithms Consistency and Linearity also work for a non-unique clause set, because the uniqueness condition has not been used anywhere. Due to limited time, we could not check this, so we only try to characterize the set of clauses for which Unskolemize works in the current form, without the extension for establishing uniqueness as described in 5.3.

To begin with, we can simply give a criterion for clause sets which is sufficient for failure of Unskolemize.

Proposition 5.5.1 If a clause C is not strongly locally linear, then it cannot be made unique by variable abstraction without destroying local linearity.

Proof. (Sketch) Consider to skolem expressions s_{1}, s_{2} with Args(s_{1}) ⊆ Args(s_{2}). Let us assume x occurs more than once in s_{1}. If we apply variable abstraction to one of its occurrences, we introduce a fresh variable which must also be introduced in s_{2}, because otherwise we loose linearity, and of course it could not be reestablished by later abstractions. Hence it is clear that s_{1} can only be made unique if we can introduce all new variables both in s_{1} and s_{2}, which is only possible if each variable occurs in s_{1} at most as often as in s_{2}. □

On the other hand, we have shown that Unique preserves strong local linearity, so that in this case, it does not destroy local linearity. We claim that a clause set M satisfying strong local linearity can be unskolemized using renaming only if Unique(M) can be unskolemized (note that the notion of strong local linearity has also been defined for clauses with nonvariable skolem function arguments). Then we are able to prove

Proposition 5.5.2 If M is a strongly locally linear, locally consistent clause set that can be made globally consistent and linear by renaming, then Unskolemize finds such a renaming.

Proof. We search for a substitution σ_{cl} which is a renaming on M such that σ_{cl}(M) is globally linear and consistent. Note that, after all clauses have been made pairwise variable disjoint by Separate , such a global renaming exists if and only if a set of local renamings (for each clause) exists that also makes M locally and globally linear.

Now assume that M is strongly locally linear, and some σ_{cl} as above exists. Intuitively, is quite clear that such a substitution also exists for M_{a} =^{def} Abstract(M), because the replacement of a term by a variable should only increases our chances to find it, as long as the term is replaced by the same variable in the whole clause (as opposed to the abstractions of occurrences Unique makes). Also, Abstract preserves strong local linearity. We do not prove these assertions.

Now we have that σ_{cl} exists for M_{a}, and that it is strongly locally linear. Our above claim was that some σ_{cl} exists also for M_{u} =^{def} Unique(M_{a}), and we now have to show that it it is found by Linearity on M_{c} =^{def} Consistency(M_{u}, &μ).

One way to see this is to observe that a consistent renaming unifies all skolem expressions headed by the same function symbol. When we regard the search for a consistent renaming as a unification problem, there is of course (under these simple conditions) a most general unifier, so any consistent renaming σ can be written as

σ = σ_{c} ∘ σ_{r},

with σ_{c} being the most general consistent renaming, and σ_{r} some substitution. Therefore, we can decompose σ_{cl}: σ_{cl} = σ_{c} ∘ σ_{l}.

Using 5.2.2, it can also be shown that Consistency computes the most general renaming σ_{c}. It was to show that Unskolemize finds σ_{cl} for M_{u}, provided it exists. If it exists, σ_{c} does exist, and by the completeness property stated in proposition 5.2.12, Consistency finds it. But then, by the completeness property 5.2.5, Linearity finds σ_{l} if and only if it exists for M_{c} =^{def} Consistency(M_{a}), which completes the proof. □

5.5.2 Time complexity

Most algorithms used by Unskolemize can be shown to have quadratic or even linear time complexity on the length of the input with any reasonable data structures and algorithms for sets and set operations. The only problem is the non-determinism we introduce when we establish uniqueness. This algorithm can indeed have exponential complexity. However, in the above section 5.5.1, we made the reasonable claim that we could get rid of this step, which would make Unskolemize an algorithm with quadratic time complexity.

5.6 Future work

Unskolemize can be seen as an inference strategy on a set of equivalence preserving rewrite rules. Therefore, we might study elimination of functions in the framework of rewrite systems: We could study inference strategies and there completeness, introduce new inference rules and examine how they combine with others etc. We could study rewrite rules used in optimized skolemization to see whether they are not only satisfiability, but also equivalence preserving. When the number of skolem functions and their arity is small, then it might even be possible to run through all combinations of rewritings of a clause set.

Alternatively, we could try to transfer the Scan method of generating sufficiently many resolvents to the problem of function elimination. I propose to design a predicate elimination algorithm that works without skolem functions. An indication that such an algorithm is not too difficult to find might be the close resemblance between C-resolution and ordinary resolution. For first-order logic, calculi working without skolem functions have been designed, and perhaps they could be “lifted” for our second-order purpose. Then we could encode skolem functions as predicates and eliminate the introduced predicates, an approach not working with Scan in its current form. This way, we could study function and predicate elimination in a uniform way. We could take advantage of methods from model theory, the theory of deductive systems and especially unification theory. Furthermore, as we have shown in chapter 4 that first-order theory proving and secondorder quantifier elimination are related in a simple way, we could then study deduction problems in first-order logic from the viewpoint of second-order quantifier elimination, which might also be elucidating, and thrilling.

Implementation of Scan and Unskolemize

This chapter contains a description of the program Scan, an implementation of the algorithms Scan and Unskolemize. The implementation is based on the code of the theorem prover Otter, a wide-spread theorem prover for first-order logic, which has been developed by William McCune ([McC90]). From Otter, Scan inherits the programming language C, basic data structures and a user interface with a comfortable, PROLOG-style parser for first-order formulas. The necessary extensions of the Otter code also use C++ constructs, making Scan a C++ program on the whole.

The three main sections of this chapter deal with a description of the user interface, a general description of the algorithms used in the implementation and a detailed description of the implementation itself.

The algorithms together with the technical details of the implementation should provide a good specification of Scan and a guide through the code. To achieve this , we also provide some information about the Otter data structures and their implementation, which has no official documentation.

The description of the user interface should give all of those who are eager to work with Scan on elimination problems a quick start.

But first we pay tribute to

6.1 The roots: Otter

Otter is short for Organized Techniques for Theorem-proving and Effective Research. The C program Otter is basically an implementation of the resolution calculus and some of its extensions.

74CHAPTER 6. IMPLEMENTATION OF SCAN AND UNSKOLEMIZE

Apart from the standard resolution rule, Otter offers more complicated inference rules like hyper-resolution and UR-resolution, paramodulation for equality reasoning and demodulation for rewriting techniques. Simplification rules like forward and back subsumption can help to remove redundancies. The inference rules are applied according to a simple set-of-support strategy, with weighing mechanisms for selecting a given clause.

To achieve a high performance, which has been an explicit design goal in the Otter development ([McC90]), Otter manages its clause set data via indexes. They are mainly used for quick retrieval of unification partners that are needed in the various occurring unification problems.

Though Otter mainly operates on clauses, it can read both formulas and clauses via a comfortable parsing mechanism. This can parse formulas with user defined operators according to their precedence and notation (infix,prefix,postfix) which can be declared by the user. Thereby, a lot of redundant parentheses can be saved, resulting in good readability and convenient notation.

6.2 Scan features and how to use them

Scan contains implementations of all simplification rules described in 4. Their use is optional. Scan has two inference strategies, one eliminating predicates in arbitrary order, leaving the choice to Scan, and one eliminating predicates successively. Results of the Scan algorithm can be minimized to eliminate clauses that are implied by others.

The user interface of Scan allows for declarations of notation type (prefix, infix, postfix) and precedence of operators to simplify input. Full information about the inference process can be printed out, or parts of it suppressed.

Scan gets as input a text file which specifies an elimination problem and options. Section 6.4.3 describes the content and the syntax of the Scan input file, and how the features described above can be used. Note that it is not possible to understand the precise effects of certain parameters, especially those influencing the inference process of Scan, without the algorithms in the next section.

6.3 Implementation of Scan

In this section, we will sketch how Scan works, which will facilitate the explanation of its user interface afterwards.

We will briefly describe the input to Scan and its main computation phases.

Scans input can be subdivided into two major parts:

• The logical part: A representation of a second-order formula, represented by a first-order formula and lists of quantified predicates and functions

• The control part: Optional control information for Scan and Unskolemize and optional control information for the user interface

Scan manages the logical information about an elimination problem in mainly three clause lists: Sos, Usable und Demodulators. Sos contains the clause form of the formula with the quantified predicates. On this list, Scan operates by drawing inferences. Usable contains clauses that are only used for subsumption and unit-deletion of clauses in Sos. This list is not modified. Demodulators contains equalities that can be used for rewriting clauses in Sos. Whether it may be modified is determined by the user: equalities that are generated during the search can be automatically added to Demodulators.

The management of control information is not important at this level of description; in the following sketch of the main Scan algorithm, we will refer to this information as “options”.

Some remarks on the algorithm:

• The variable ElMode is part of the options and determines the order in which predicates are eliminated: Either one after the other, and according to their position in P redList, or in arbitrary order, leaving free choice of the next pure clause to Scan.

• The procedure PurifyLit and RemoveRedundancy do roughly what one expects, their interns are described below. So is the procedure PreProcessInput, which basically normalizes the input with respect to some simplification rules.

• We write ’&’ in front of parameters to denote a call by reference which may change the parameter

See figure 6.1 for the algorithm.

Algorithm 6.3.1 (Scan)

list<clause> sos, usable; list<predicate> P redList; clause P ureCl; literal P ureLit; formula Result; // read information from input file ReadInput(&Sos, &Usable, &P redList, &F nList, &Options) // process Sos and Usable ProcessInput(&Sos, &Usable); // Apply extended purification rule to Sos XPurify(Sos, &P redList); // Get first clause to be purified SelectFirstPureLit(&P ureCl, &P ureLit, ElMode, &P redList, &found); // as long as there is a literal to be purified . . .. While (found){

PurifyLit(P ureCl, P ureLit);

XPurify(Sos, &P redList);
SelectNextPureLit(&P ureCl, &P ureLit,
ElMode, &P redList, &found); }

// remove redundant clauses in the Sos RemoveRedundancy(&Sos); // eliminate skolem functions Let Result = Usk(&Sos, F nList); Output(Result);

Figure 6.1: The basic algorithm of Scan Algorithm 6.3.2

RemoveRedundancies( list<clause> &Sos)

list<clause> P assed; // clauses that passed the test clause Goal; // the clause to be proven // Sort clauses according to their length, longest to the beginning SortByLength(Sos) While (!Empty(Sos)){

Let Goal = Car(Sos); Let Sos = Cdr(Sos); If (Goal can be proven from Sos in a limited time) then Let P assed = Append(Sos, Goal); }

Let Sos = P assed;

Return;

Figure 6.2: The redundancy check of Scan

RemoveRedundancies The procedure RemoveRedundancies uses a simple but sometimes quite effective check for redundant clauses. It tries to prove each clause from the rest of the clause set, see figure 6.2. For the proof of a clause, Otter is invoked for some time set by the user in the options, see 6.4.3.4. The details of this option are described in 6.5.3.

PurifyLit The procedure PurifyLit purifies a literal in a clause and checks generated C-resolvents for redundancies. Its redundancy check Pre-ProcessCl, again explained below, is an extension of the Otter procedure pre process, see [McC90] and 6.5. Actually, it is not only a redundancy check but also sometimes infers new clauses. The procedure PostProcessList generates C-factors and extends the Otter procedure post process all. See figure 6.3 for the algorithm.

Note that it is not necessary to check whether a factor of a resolvent Res back subsumes P ureCl, because then Res also back subsumes P ureCl, and this has been checked before.

PreProcessInput, PreProcess and PostProcess The procedure PreProcess takes a clause and a clause list as parameters. It adds the clause to the set if it passes several redundancy tests. Figure 6.4 describes the algorithm.

The procedure PreProcessInput takes clauses from the clause list given Algorithm 6.3.3

PurifyLit( clause P ureCl, literal P ureLit) list<clause> Kept; // Flag for: PureCl has been back subsumed by one of its resolvents boole P ureBackSubsumed; Let Kept = Nil; Resolve P ureCl with every clause in Sos For (Every resolvent Res in Sos) Do {

// check redundancy, stop if P ureCL is back subsumed // non-redundant clauses are added to Kept PreProcess(&Res, &Kept); If (Res has been kept and back subsumes P ureCl)

then ExitLoop; } // Now generate factors and append them to kept PostProcess(&Kept); Append(&Sos, &Kept); Return;

Figure 6.3: Purification of literals as parameter and again adds them to the clause set as if they where inferred clauses. That is, the clauses are filtered by the procedure PreProcess.

In the following algorithms, all steps that are optional are marked by ’*’.

Algorithm 6.3.4 (PreProcess)

boole PreProcess( clause Res, list<clause> ClList)

Push constraints of Res into its literals;

∗ Demodulate Res;
∗ Orient equalities;
∗ // Delete literals in Res that can be matched with units in Sos
∗ UnitDel(Sos, Res);

Merge identical literals in Res;

∗ Apply factor simplification to Res;

If (Res is a tautology)

then Return(false);

∗ Sort literals;
∗ If (Res is subsumed by some clause in Sos or Usable)

then Exit();

∗ If (Res can be proven from Sos)

then Exit(); If (a stop condition has been fulfilled) // Especially if time limit has been exceeded

then Exit(); // Now keep clause Append(Res, ClList); If (|Res|) = 1)

then{ Check for unit conflict with other unit literals,

add empty clause if proof has been found; } If (Res is the empty clause or a proof has been found previously) then Print the proof;

∗ If possible, make Res a demodulator;
∗ Return(true);

Figure 6.4: Preprocessing of generated clauses

The proof checking is another inheritance from Otter. It helps to detect unsatisfiable clause sets more quickly.

Finally, the procedure PostProcess, see figure 6.5, finishes the process-Algorithm 6.3.5 (PostProcess)

boole PostProcess( list<clause> &Kept)

For (all clauses C in Kept) Do { If (C has been made a demodulator by PreProcess) Back demodulate clauses in Sos and Usable ; Discard clauses in Sos that are (back) subsumed by Res; // Generate all C-factors For (all C-factors CF ac of C) Do {

// Append C-factors if they pass retention test; PreProcess(&CF ac, &Kept); }}

Figure 6.5: Postprocessing of generated clauses

ing of a clause by generating all its C-factors, and doing back subsumption and back demodulation.

6.4 The user interface

The user interface of Scan has been taken over completely from Otter, with only minor modifications. Similarly, we could have taken over the Otter documentation of the user interface with some modifications. However, this would have resulted in quite a lot of patching and referencing, so we decided to write a new introduction. This might slow down frequent Otter users, but also speed up those who are unacquainted with Otter.

Scan can be used quickly and intuitively, though the documentation of all its features is quite big and its full syntax quite complex. Therefore, we will start with two small example that illustrate how to eliminate function and predicate quantifiers with Scan.

6.4.1 A quick example

Let the formula

∃P ∀x∃y (P (x) ∨ R(x, y)) ∧ (Q(x, y) ∧ ¬P (a))

be given, which we want to reduce to first-order logic. A corresponding input file for Scan might look like this:

Example 6.4.1

% set \so{} variable lists
pred_list[P(_)]. % specify predicates to be eliminated
% set options
% flags
set(unskolemize). % activate unskolemization
% parameters
assign(minimize_at_end_time,1). % try to prove clauses in result redundant,
                                % one second for each proof attempt
% write result into log file name
logfile("doc1_example.log").
% elimination problem in formula form
formula_list(sos).
(all x exists y ( (P(x) | R(x,y)) & (Q(x,y) & -P(a)) )).
end_of_list.

We start Scan with

Scan < scan example1.in > scan example1.out.

At the end of the output file ‘scan example1.out’ or in the log file, we find the result:

% result of Scan:
list(usable).
2 [] Q(x,$f1(x)).
4 [binary_c_res,1.1,3.1] R(a,$f1(a)).
end_of_list.
% result of unskolemization:
(all x0 exists e0 (Q(x0,e0) & (R(x0,e0) | x0 != a)))
% Clause set unskolemized.

The Scan algorithm may not terminate. Like in theorem proving, one sometimes has to be patient to get a solution. The Unskolemize algorithm always terminates, but may fail to remove the quantified functions.

The rest of the output file contains information about Scan’s inference process. The section 6.4.3.4 describes how to control the amount of information that is given.

6.4.2 Using Scan: The shell level

Scan takes as input an elimination problem, whose specification is described in the following sections . Then it applies Scan or Unskolemize or both algorithms to the input, and outputs information about the computation process of the selected algorithms. Finally, Scan outputs the results of the algorithms.

Input is read from the standard input, which normally is the keyboard, and written to standard output, which normally is the screen. In practice, the input will of course usually be coded in a file, and the output should be available in file form, too. In this situation, the standard input and output streams must be redirected. On a Unix system, an appropriate Scan invocation reads like this:

Scan < inputfile > outputfile.

The mere result, without any information about the computation process, can be output on a file with a special command, see the following 6.4.3.

6.4.3 The input file: Specifying elimination problems

This section describes in general terms how to use Scan input files for specifying elimination problems. It should be easily understood with the example 6.4.1 in mind. In describing the input file, we will follow Otter terminology.

The input file contains

• commands for specifying control information, and

• lists of predicates, functions, or logical statements in clause or formula form specifying logical information.

The order in which information is given in the input file is usually not relevant.

Control information Roughly speaking, control information can either concern the user interface or the elimination algorithms and their output etc.

Control parameters for algorithms tell Scan 6.4. THE USER INTERFACE 83

• which algorithm, Scan or Unskolemize to apply to the logical input • which inference strategy to select

• which inference rules to use

• which resources like time and memory to limit

• how to index clauses for retrieval

• which information to output The Scan control parameters for algorithms are listed and explained in

6.4.3.4.

Parsing control information tells the parser

• the declaration of operators

• whether to check for use of symbols with multiple arities

• what terms to recognize as variables in clauses A.5 explains how to declare and use operators. The remaining parsing

control parameters are described in 6.4.3.3.

Commands have the form <command name>(<par_{1}>, …, <par_{n}>). Like Otter, Scan understands only a few commands:

• set, clear and assign, to specify options specify beginning and end of clause and formula lists

• include(<file name>) to include another file. Scan distinguishes two types of options, namely flags and parame-

ters. Flags are boolean-valued options, that are activated by the command set(<flag name>) and deactivated by clear(<flag name>) Parameters are integer-valued options, that are assigned a value by

assign(<parameter name>, <value>).

Logical information Lists contain the first-order part of an elimination problem, and contain either logical statements, which represent the firstorder formula of a second-order formula, or function or predicate variables, which are then interpreted as quantified in the lists with logical statements.

The list Sos contains the first-order part of a formula. Usable contains clauses that are used for subsumption, but not for inferring new clauses, and Demodulators contains a list of demodulators. For the use of demodulators, we refer to the Otter manual [McC90].

Formula and clause lists have the form

list(<list name>).<sequence of clauses> end of list.

or formula list(<list name>).<sequence of formulas> end of list.

where

<sequence of clauses> → ε | <clause>. <sequence of clauses> <sequence of formulas> → ε | <formulas>. <sequence of formulas>

Possible list names are Sos, Usable and Demodulators.

Clauses and formulas can be written down quite naturally. Formulas must always be closed. We will give an example below, and their exact syntax in 6.4.3.2.

Finally, predicate and function lists contain predicates and functions with dummy arguments, marked by ’ ’:

skolem([f( , ), g( )]). for skolem functions

pred list([P, Q( , , ), R( )]). for predicate variables

6.4.3.1 General syntax

An input file is a sequence of Otter terms which must be terminated by a point ’.’. Formulas, clauses and commands are specializations of this term type. OTTER terms may contain unary and binary operators, for which precedence and notation type (prefix,infix, postfix) can be declared as described in A.5. Comments reach from ’%’ to the end of the line.

Terms are called complex when they have subterms, and simple, when they have none.

6.4.3.2 Syntax of formulas and clauses

Formulas and clauses are built up as usual from atoms and a set of logical operators and can be written down quite naturally. Clauses are disjunctions of literals without explicit quantification of variables, while all variables in formulas have to be quantified. This raises the question how variables can be told from constants in clauses. Otter solves this problem by assuming all arguments that start by u,v,w,x,y or z to be variables. As an example:

% a is a constant
list(sos). P(x,y) | Q(a) | R(f(b,y2)). end_of_list.
% a is a variable
formula_list(sos).
all a x y y2 (P(x,y) | Q(a) | R(f(b,y2))).
end_of_list.

The exact syntax of formulas and clauses can be found in the appendix. The text has been copied almost literally from the Otter user manual.

6.4.3.3 Parsing control parameters

Option  Type Default Description

check arity Flag set If set, all symbols in the input

file must have fixed arity

prolog style variables Flag clear If set, terms without arguments in clauses are identified as a variable iff the start with A through Z (upper case) or with .

6.4.3.4 Control parameters

Selecting algorithms Scan applies Scan and Unskolemize one after the other to the input formula sets. Both algorithms can separately be enabled and disabled.

Option  Type  Default  Description
scan  Flag  set  If set, apply Scan to input
unskolemize  Flag  clear  If set, apply Unskolemize to

output of Scan

Inference strategy The choice among inference strategies is not so big yet. As described in 6.3, the user can choose to eliminate the predicates one after another as they occur in the list of predicate variables, leave the choice to Scan.

Option  Type  Default  Description
succ elimination  Flag  clear  If set, eliminate predicate

variables one after another as they are listed. If clear, elimination order is arbitrary

Inference rules The Scan optional inference rules fall roughly into two categories: rules for deriving new clauses, rules for simplifying the clause set or single clauses in some way, and rules for normalizing clauses in some way. Apart from clauses resulting from demodulation, new clauses are generated by the C-factoring and binary C-resolution rule. When the C-resolution rule is disabled, the Scan algorithm is disabled. Simplifications are done by forward and backward subsumption, unit deletion and factor simplification. Forward subsumption is available in a simple and an extended form, as described in 6.3. Optional normalizing is restricted to orienting equalities and sorting of literals.

Unlike in theorem provers, it is usually a good choice to activate all available inference rules of Scan, and they are activated by default, except for extended forward subsumption, as it is quite time consuming. However, they can be deactivated for special purposes, for example to achieve different but equivalent results. Figure 6.6 lists options concerning inference rules.

Option  Type  Default Description
binary c res  Flag  Set  If set, use binary C-resolution
c factor  Flag  Set  If set, apply C-factorization

and factor simplification

unit deletion Flag Set If set, apply unit deletion check redundancy Param 0 set time for redundancy check

of a generated clause in seconds.

sort literals Flag Clear sort literals of generated clauses: first negative literals, then positive literals. May speed up subsumption.

Figure 6.6: Scan inference rules Resources The amount of time and space that Scan may consume can be roughly limited. Scan stops more precisely than Otter when resource limits are exceeded. See figure 6.7.

Option  Type  Default  Description
max seconds  Param  -1  If value is -1, then there is

no time limit for Scan, otherwise it stops after n seconds, where n is the integer value of max seconds

max mem Param -1 If value is -1, then there is no memory limit for Scan, otherwise it stops before more than n kilobytes have been allocated, where n is the integer value of max mem

Figure 6.7: Scan resource control options

Output The main purpose of Scan’s output is to show its result, and to document every inference step, thus making its result verifiable. The output parameters are listed in figure 6.8.

Indexing Indexes allow for quicker forward and backward subsumption und unit deletion. Scan has inherited two index types from Otter: FPA indexing and discrimination tree indexing (See also 6.5). While back subsumption is always done with discrimination trees, the user has the choice in the case of forward subsumption.

FPA indexing is usually much slower than discrimination tree indexing, while discrimination tree indexing may require a lot more memory then FPA indexing. The index type has no influence on the result of Scan, especially not on its termination.

For FPA indexing, the accuracy of retrieval results can be influenced by the indexing depth. A higher indexing depth needs more memory and more time for indexing, but retrieval can be much faster. Figure 6.9 lists indexing options.

Option  Type  Default  Description
very verbose  Flag  clear  If set, output much informa-

tion about inference process

print given Flag clear If set, print selected pure

clause

print kept Flag set If set, print generated clauses that are actually added to a clause set

print back sub Flag set If set, print clauses that are back subsumed. During input processing, back subsumed clauses are always printed (see 6.5)

print new demod Flag set If this flag is set, clauses are printed as they are back demodulated. Backdemodulated clauses are always printed during input processing (see 6.5.

display terms Flag clear If this flag is set, all clauses and terms are printed in pure prefix form (Sec. A.2).

pretty print Flag clear If this flag is set, clauses are output in an indented form that is sometimes easier to read. The parameter pretty print indent (default 4) specifies the number of spaces for each indent level.

bird print Flag clear If this flag is set, terms constructed with the binary function a are output in combinatory logic notation (without the function symbol a, and left associated unless otherwise indicated). For example, the clause a(a(a(S, x), y), z) = a(a(x, z), a(y, z)) is output as Sxyz = xz(yz).

Figure 6.8: Scan output parameters

Option  Type  Default  Description
for sub fpa  Flag  clear  If set, use FPA indexing for

forward subsumption, otherwise discrimination tree indexing

fpa literals parameter 8 Sets indexing depth from 0 to 100

Figure 6.9: Indexing options

6.5 Details of the implementation

6.5.1 Using OTTER for building Scan

Otter has been used in two ways for Scan:

• As a collection of data structures and techniques for theorem proving

• As a complete theorem prover that is used in subprocesses to prove clauses redundant

In fact, the code of Scan contains the full Otter code, with some patches of course. The main part of this section will focus on the first point and show how parts of Otter have been reused in Scan. This was also the more difficult part of the implementation. We will show this on an abstract level, regarding Otter as a clean implementation of several data structures and algorithms based on these structures. This allows for a very simple presentation. However, Otter has not been implemented that cleanly, and quite some low-level patches were necessary to use Otter code for our purposes.

The Scan implementation can roughly be subdivided into three major parts:

• The user interface

• The implementation of Scan

• The implementation of Unskolemize

We have already mentioned that the user interface of Scan is nearly identical to that of OTTER. The minor modifications can be traced in the code. The implementation of the Unskolemize algorithm uses its own data structures, especially an own term data structure. Communication with the Otter parts is provided by conversion routines for both term types. Therefore, we will restrict ourselves to describing the implementation of Scan using Otter algorithms.

6.5.2 Using Otter algorithms and data types for implementing Scan

Scan uses many of Otter’s data types. In contrast to some of the reused Otter algorithms, none of them had to be modified. For implementation of Scan, the Otter clause management and its inference process is central, so let us first have a look at them.

Otter clause management Otter’s main data type for drawing inferences is the clause data type. Though there is a formula data type for representing input formulas, these formulas are converted into clause form before the inference process starts. Otter’s uses structure sharing on terms for efficient clause storage and term indexing for efficient clause retrieval in unification problems. For different purposes, several indexing techniques are available, namely FPA-indexing and discrimination tree indexing. ^{1}

Otter’s inference process The structure of Otter’s inference process is quite simple. We present it under the aspect of the Otter clause management, which is important for understanding its reuse in Scan. Also, we reduce Otter to a simple binary resolution system with factoring, which can in fact be done by setting options accordingly. This was the starting point of the original code analysis: We wanted to obtain Scan simply by to replacing ordinary resolution with C-resolution and factoring with Cfactoring. Figure 6.10 describes Otter’s inference process.

The processing of newly generated clauses in Otter, like in Scan is divided into the pre- and postprocessing phase. Both will be described more precisely in the next paragraph. Roughly speaking, preprocessing, which is done by the OtterPreProcess-Procedure, includes demodulation,unitdeletion and checks whether the resolvent is forward subsumed by a clause Algorithm 6.5.1

1Structure sharing of terms tries to save space by storing common subterms of several terms only once. Term indexing is a means for quick retrieval of terms in unification problems. By techniques that may also be seen as structure sharing, term sets are organized in such a way that it is possible to quickly retrieve, say, all the terms in the set unifying with or matching f(x, g(y)).

Read input; Transform input into clause lists Sos and Usable; Integrate and index all clauses While (Sos is not empty and no refutation has been found)

Pick the “lightest” clause given clause from Sos While (There are resolution partners forgiven clause)

Get a resolution partner for given clause from Usable using the term index and generate the resolvent Res; // Now try several redundancy tests on Res. // If it passes all of them, append it to Sos, // index and integrate it. OtterPreProcess(Res); // (Details below)

// After all resolvents with given clause // have been made, build factors and do back subsumption For (All generated resolvents Res) Do {

OtterPostProcess(Res)} // (Details below)

Figure 6.10: Otter’s inference process in Sos,Usable or Passive. Then the resolvent is integrated. The postprocessing (OtterPostProcess) eliminates clauses from Sos and Usable that are back subsumed by the new clause and generates its factors, which are in turn pre- and postprocessed. Back subsumed clauses are unindexed and disintegrated. The separation into pre- and postprocessing is in part a consequence of the indexing and structure sharing of terms: Since term integration is expensive, a clause is only integrated and indexed if it is surely kept and not changed anymore.

Modifying Otter to implement Scan As we’ve said, the original approach to reusing Otter for a primitive implementation of Scan was: Replace standard binary resolution with C-resolution and standard factorization with C-factorization. Or rather, extend Otter with these new inference rules by copying and modifying the code for the similar old ones. However, the simplified set-of-support inference strategy that Otter uses when the given clause has been selected is not compatible with the Scan algorithm, as the given clause must be resolved with all clauses, not only those in Usable, especially not with itself. Therefore, the inference algorithm of Scan has been implemented independently of the Otter inference algorithm, but using the Otter clause management. The Otter processing of inferred clauses could be used with some modifications, on the basis of the original Otter data structures for clause management. We will describe the most important of those modifications in the following.

It has been possible to modify Otter so smoothly that the new preand postprocessing facilities are compatible with all other Otter processing facilities. Therefore, the Otter facilities can still be used by setting options that influence pre- and postprocessing. If they are not mentioned in this documentation, they did not seem very useful in the context of quantifier elimination, or only in very special cases or with much knowledge about Otter. Especially, we do not describe the use of user-defined evaluable predicates, which allow for very refined control. Still, all these facilities can be used exactly in the same way as they are described in the Otter manual if it turns out to be useful.

We begin with the modifications to Otter’s preprocessing. We leave out computation steps that are not relevant in this context. These are mainly the evaluation of user-defined predicates and the deletion of clauses whose user-defined weight has exceeded a certain limit or who contain identical nested skolem functions. A full account of the Otter preprocessing steps can be found in the Otter manual.

We look backwards and obtain OtterPreProcess from Scan’s Pre-Process as described in 6.3 by simply deleting three steps:

• Constraint elimination

• Extended forward subsumption of clauses that can be proven from Sos

• The check for stop conditions

Constraint elimination and extended forward subsumption are of course required by the Scan algorithm. The new check for stop conditions was not necessary, but reasonable to obey time limits more precisely. This is an obvious advantage anyway, but has especially been motivated by the timing of the extended forward subsumption. For details, see section 6.5.3.

During the preprocessing in both Otter and SCAN, kept clauses are integrated and indexed. This is done after the kept clause has been appended to Sos.

Otter’s postprocessing is very similar to Scan’s. Only the standard factorization of Otter has been replaced by the C-factorization necessary for Scan.

6.5.3 Using Otter for proving clauses redundant

For the extended forward subsumption test and the minimization of the clause set at the end of the elimination process, Scan uses Otter’s theorem proving abilities. We describe the case of extended forward subsumption. Minimization is done in a similar, though not identical way.

Given a newly generated clause C, Otter has to be invoked with the current Sos of Scan and the negation of C in its own Sos. Of course, this could be done by using the Otter user interface, that is, by writing the input clause set to a file, starting Otter on this input and extracting the result from the output file. However, this is quite a waste of time, as the clause set already has the internal representation that is used by Otter. Especially, it is already indexed and integrated, that is, the Otter inference process could at once start on a memory copy of this clause set (one copy has of course to be kept).

However, things are not that simple. Though this solution is possible, it requires a lot of changes in the Otter sources. We made a compromise which turned out to be quite effective. It depends on the multitasking architecture of Unix systems.

When a new clause C has to be checked for redundancy, a new subprocess of the Scan process is generated which is an exact copy of its father process by the fork() system command. In particular, it inherits a copy of the Sos of Scan. Essentially, these clause sets are now emptied, copied and filled with the clauses from their copies again as if they were input clauses. Before, some Otter options are set for activating options that are deactivated during quantifier elimination. Especially, Otter’s auto mode is activated, which analyses input clause sets and automatically selects inference rules which seem appropriate. Then Otter is run for a limited time given by the parameter check redundancy time. The result of its search is communicated to its father process, and C is eliminated if Otter has found a proof.

This method required a change in the Otter preprocessing which has been mentioned in the previous section. The original OTTER checks its stop conditions, in particular its computation time limit, after all resolvents of the given clause have been postprocessed. Recall that postprocessing of these resolvents means that all their factors are generated and again pre- and postprocessed. This can take a lot of time, during which the time limit is not checked and may well be exceeded. This inaccuracy is of course multiplied when Scan invokes Otter every time a new clause is generated. To keep the behavior of Scan a little more predictable, now Otter’s modified preprocessing checks the stop conditions. During postprocessing, all generated factors are preprocessed, so that the time limit is now obeyed there.

6.6 Modules and source files

As Otter is not cleanly modularized, and due to some necessary patches, clean modularization of Scan would only have been possible with structural changes of the source files much bigger than the current. However, modulo some patches, the whole implementation can roughly be subdivided into the Otter, Scan and Unskolemize. Source files are divided into pure Otter files, patched Otter files, Otter file patch files (!), files for the implementation of Scan and files for the implementation of Unskolemize. The file type can easily be identified:

• Files with the prefix ‘scan’, like ‘scan Proving.c’ are part of the implementation of Scan

• Files with the prefix ‘us’, like ‘us RelationVnPos’ are part of the implementation of Unskolemize • Files with no prefix (without underscore in the name), like ‘main.c’

belong to Otter. They are patched if a corresponding patch file exists, and pure otherwise

• Files with the prefix ‘Patch’ contain patches for the Otter file named in the suffix, like ‘Patch misc.c’ which patches ‘misc.c’ of Otter

Lines of Otter files that have been modified or added are marked by the label ’SCAN PATCH’ or, in the case of complicated patches, preceded by this label.

6.7 Installation

The installation of Scan is described in the INSTALL file that comes with the sources.

96CHAPTER 6. IMPLEMENTATION OF SCAN AND UNSKOLEMIZE

Appendix A

Syntax of formulas and clauses in Scan

A.1 Names for Variables, Constants, Functions, and Predicates

Three kinds of character string, collectively referred to as names, can be used for variables, constants, function symbols, and predicate symbols:

• An ordinary name is a string of alphanumerics, $, and _.

• A special name is a string of characters in the set *+-/\^<>=`~:?@&!;# (and sometimes |).

• A quoted name is any string enclosed in two quotation marks of the same type, either " or '. We have no trick for including a quotation mark of the same type in a quoted name.

(The reason for separating ordinary and special names has to do with infix, prefix, and postfix operators; see Sec. A.5 in the Otter manual.) Although out of place here, for completeness we list the meanings of the remaining printable characters.

• . (period) — terminates input expressions.

• % — starts a comment (which ends with the end of the line).

• ,()[]{} (and sometimes |) — are punctuation and grouping symbols.

98APPENDIX A. SYNTAX OF FORMULAS AND CLAUSES IN SCAN

Variables. Determining whether a simple term is a constant or a variable depends on the context of the term. If it occurs in a clause, the symbol determines the type: the default rule is that a simple term is a variable if it starts with u, v, w, x, y, or z. If the flag prolog_style_variables is set, a simple term is a variable if and only if it starts with an upper-case letter or with _. (Therefore, variables in clauses must be ordinary names.) A simple term in a formula is a variable if and only if it is bound by a quantifier.

Reserved and Built-in Names. Names that start with $ are reserved for special purposes, including evaluable functions and predicates, answer literals and terms (see Otter manual), and some internal system names. The name = and any name that starts with eq, EQ, or Eq, when used as a binary predicate symbol, is recognized as an equality predicate by the demodulation and paramodulation processes. And some names, when they occur in clauses or formulas, are recognized as logic symbols.

Overloaded Symbols. The user can use a name for more than one purpose, for example as a constant and as a 5-ary predicate symbol. When the flag check_arity is set (the default), the user is warned about such uses. Some built-in names are also overloaded; for example, | is used both for disjunction and as Prolog-style list punctuation, and although - is built in as logical negation, it is generally used for both unary and binary minus as well.

A.2 Terms and Atoms

Recall that, when interpreted, terms are evaluated as objects in some domain, and atoms are evaluated as truth values. Constants and variables are terms. An n-ary function symbol applied to n terms is also a term. An n-ary predicate symbol applied to n terms is an atom. A nullary predicate symbol (also referred to as a propositional variable) is also an atom.

The pure way of writing complex terms and atoms is with standard application: the function or predicate symbol, opening parenthesis, arguments separated by commas, then closing parenthesis, for example, f(a,b,c) and =(f(x,e),x). If all subterms of a term are written with standard application, the term is in pure prefix form. Whitespace (spaces, tabs, newlines, and comments) can appear in standard application terms anywhere except between a function or predicate symbol and its opening parenthesis. If the flag display_terms is set, Otter will output terms in pure prefix form.

Infix Equality. Some binary functors can be written in infix form; the most important is =. In addition, a negated equality, -(a=b) can be abbreviated a!=b.

List Notation. Prolog-style list notation can be used to write terms that represent lists. Table A.1 in the Otter manual gives some example terms in list notation and the corresponding pure prefix form. Of course, lists can

      []         $nil
      [x|y]      $cons(x,y)
      [x,y]      $cons(x,$cons(y,$nil))
      [a,b,c,d]  $cons(a,$cons(b,$cons(c,$cons(d,$nil))))
      [a,b,c|x]  $cons(a,$cons(b,$cons(c,x)))

Table A.1: List Notation

contain complex terms, including other lists.

A.3 Literals and Clauses

A literal is either an atom or the negation of an atom. A clause is a disjunction of literals. The built-in symbols for negation and disjunction are - and |, respectively. Although clauses can be written in pure prefix form, with - as a unary symbol and | as a binary symbol, they are rarely written that way. Instead, they are almost always written in infix form, without parentheses. For example, the following is a clause in both forms.

   Pure prefix:  |(-(a),|(=(b1,b2),-(=(c1,c2))))

Infix (abbreviated): -a | b1=b2 | c1!=c2

Otter accepts both forms. (Clauses are parsed by the general term-parsing mechanism presented in Sec. A.5).

A.4 Formulas

Table A.2 lists the built-in logic symbols for constructing formulas.

Formulas in Pure Prefix Form. Although the practice is rarely done, formulas can be written in pure prefix form. Quantification is the only tricky part: there is a special variable-arity functor, $Quantified, for quantified formulas. For example, ∀xy∃z(P (x, y, z)|Q(x, z)) is represented by

negation  -
disjunction  |
conjunction  &
implication  ->
equivalence  <->
existential quantification exists
universal quantification all

Table A.2: Logic Symbols

     $Quantified(all,x,y,exists,z,|(P(x,y,z),Q(x,z))).

If the flag display_terms is set, the formulas (and everything else) will be displayed in pure prefix form.

Abbreviated Formulas. Formulas are usually abbreviated in a natural way. The associativity and precedence rules for abbreviating formulas and the mechanism for parsing formulas are presented in Sec. A.5. Here are some examples.

standard usage Otter syntax (abbreviated)

  ∀xP (x)  all x P(x)
  ∀xy∃z(P (x, y, z) ∨ Q(x, z))  all x y exists z (P(x,y,z) | Q(x,z))
  ∀x(P (x) ∧ Q(x) ∧ R(x) → S(x))  all x (P(x) & Q(x) & R(x) -> S(x))

Note that if a formula has a string of identical quantifiers, all but the first can be dropped. For example, all x all y all z p(x,y,z) can be shortened to all x y z p(x,y,z). In expressions involving the associative operations & and |, extra parentheses can be dropped. Moreover, a default precedence on the logic symbols allows us to drop more parentheses: <-> has the same precedence as ->, and the rest in decreasing order are ->, |, &, -. Greater precedence means closer to the root of the term (i.e., larger scope). For example, p | -q & r -> -s | t represents (p | (-(q) & r)) -> (-(s) | t), or in pure prefix form,

->(|(p,&(-(q),r)),|(-(s),t)).

When in doubt about how a particular string will be parsed, one can simply add additional parentheses and/or test the string by having Otter read it and then display it in pure prefix form. The following input file can be used to test the preceding example.

    assign(stats_level, 0).

    set(display_terms).
    formula_list(usable).
    p| -q&r-> -s|t.       % This formula has minimum whitespace.
    end_of_list.

In general, whitespace is required around all and exists and to the left of -; otherwise, whitespace around the logic symbols can be removed. See Sec. A.5 for the rules.

A.5 Infix, Prefix, and Postfix Expressions

Many Prolog systems (for example Quintus and Sicstus) have a feature that allows users to declare that particular function or predicate symbols are infix, prefix, or postfix and to specify a precedence and associativity so that parentheses can sometimes be dropped. Otter has a similar feature. In fact, the clause and formula parsing routines use the feature. Users who use only the predeclared logic operators for clauses and formulas and the predeclared infix equality = can skip the rest of this section.

Prolog users who are familiar with the declaration mechanism should note the following differences between the Quintus/Sicstus mechanism and Otter’s.

• The predeclared operators are different. See Table A.3.

• Otter does not treat comma as an operator; in particular, a,b,c cannot be a term, as in a,b,c -> d,e,f.

• Otter treats the quantifiers all and exists as special cases, because they don’t seem to fit neatly into the standard Prolog mechanism.

• Otter requires whitespace in some cases where the Prologs do not.

Functors to be treated in this special way are given a type and a precedence. Either Otter predeclares the functor’s properties, or the user gives Otter a command of one of the forms

     op(precedence, type, functor).
     op(precedence, type, list-of-functors).

The precedence is an integer i, 0 < i < 1000, and type is one of the following: xfx, xfy, yfx (infix), fx, fy (prefix), xf, yf (postfix). See Table A.3 for the commands corresponding to the predeclared functors.

op(800, xfx, ->).   op(700, xfx, @<).
op(800, xfx, <->).  op(700, xfx, @>).
op(790, xfy, |).    op(700, xfx, @<=).
op(780, xfy, &).    op(700, xfx, @>=).
op(700, xfx, =).    op(500, xfy, +).
op(700, xfx, !=).   op(500, xfx, -).
op(700, xfx, <).    op(500, fx, +).
op(700, xfx, >).    op(500, fx, -).

op(700, xfx, <=).

op(700, xfx, >=).   op(400, xfy, *).
op(700, xfx, ==).   op(400, xfx, /).
op(700, xfx, =/=).  op(300, xfx, mod).

Table A.3: Predeclared Functors

Given an expression that looks like it might be associated in a number of ways, the relative precedence of the operators determines, in part, how it is associated. A functor with higher precedence is more dominant (closer to the root of the term), and one with lower precedence binds more tightly. For example, the functors ->, |, &, and - have decreasing precedence; therefore the expression p & - q | r -> s is understood as ((p & (-q)) | r) -> s.

In each of the types, f represents the functor, and x and y, which represent the expressions to which the functor applies, specify how terms are associated. Given an expression involving functors of the same precedence, the types of the functors determines, in part, the association. See Table A.4. The following are examples of associativity:

xfx infix (binary) don’t associate
xfy infix (binary) associate right
yfx infix (binary) associate left
fx prefix (unary) don’t associate
fy prefix (unary) associate
xf postfix (unary) don’t associate
yx postfix (unary) associate

Table A.4: Functor Types

• If + has type xfy, then a+b+c+d is understood as a+(b+(c+d)).

• If -> has type xfx, then a->b->c is not well formed.

• If - has type fy, then - - -p is understood as -(-(-(p))). (The spaces are necessary; otherwise, --- will be parsed as single name.)

• If - has type fx, then - - -p is not well formed.

Caution: The associativity specifications in the infix functor declarations say nothing about the logical associativity of the operation, e.g., whether (a+b)+c is the same object as as a+(b+c). The specifications are only about parsing ambiguous expressions. In most cases, when an operator is xfy or yfx, it is also logically associative, but the logical associativity is handled separately; it is built-in in the case of the logic symbols | and & in Otter clauses and formulas, and it must be axiomatized in other cases.

Details of the Functor Declarations. (This paragraph can be skipped by most users.) The precedence of functors extends to the precedence of expressions in the following way. The precedence of an atomic, parenthesized, or standard application expression is 0. Respective examples are p, (x+y), and p(a+b,c,d). The precedence of a (well-formed) nonparenthesized nonatomic expression is the same as the precedence of the root functor. For example, a&b has the precedence of &, and a&b|c has the precedence of the greater functor. In the type specifications, x represents an expression of lower precedence than the functor, and y represents an expression with precedence less than or equal to the functor. Consider a+b+c, where + has type xfy; if association is to the left, then the second occurrence of + does not fit the type, because a+b, which corresponds to x, does not have a lower precedence than +; if association is to the right, then all is well. If we extend the example, under the declarations op(700, xfx, =) and op(500, xfy, +), the expression a+b+c=d+e must be understood as

(a+ (b+c))= (d+e).

A.6 Whitespace in Expressions

The reason for separating ordinary names from special names (Sec. A.1) is so that some whitespace (spaces, tabs, newline, and comments) can be removed. We can write a+b+c (instead of having to write a + b + c), because “a+b+c” cannot be a name, that is, it must be parsed into five names. Caution. There is a deficiency in Otter’s parser having to do with whitespace between a name and opening parenthesis. The rule to use is: Insert some white space if and only if it is not a standard application. For example, the two pieces of white space in (a+ (b+c))= (d+e) are required, and no white space is allowed after f or g in f(x,g(x)).

A.7 Bugs, etc., in Input and Output of Expressions

• The symbol | is either Prolog-style list punctuation or part of a special name. With the built-in declaration of | as infix, the term [a|b] is ambiguous, with possible interpretations t_{1} =$cons(a,b) and t_{2} =$cons(|(a,b),$nil). Otter recognizes [a|b] as t_{1}. The term t_{2} can be written [(a|b)]. The bug is that t_{2} will be output without the parentheses. This is the only case I know in which Otter cannot correctly read a term it has written.

• A term consisting of a unary + or - applied to a nonnegative integer is always translated to a constant.

• Parsing large terms without parentheses, say a1+a2+a3+...+a1000, can be very slow if the operator is left associative (yfx). If you intend to parse such terms, make the operator right associative (xyf).

• Quoted strings cannot contain a quotation mark of the same type.

• The flag check_arity sometimes issues warnings when it should not.

• Braces ({}) can be used to group input expressions, but Otter always uses ordinary parentheses on output.

A.8 Examples of Operator Declarations

Group Theory. Suppose we like to see group theory expressions in the form (ab^{−1}c^{−1−1})^{−1}, in which right association is assumed. We can approximate this for Otter with (a*b^*c^^)^. (We have to make the group operator explicit; -1 is not a legal Otter name; the whitespace shown is required.) The declarations op(400, xfy, *) and op(350, yf, ^) suffice. Other examples of expressions (with minimum whitespace) using these

declarations are (x*y)*z=x*y*z and (y*x)^=x^*y^.

Otter Options. Options are normally input as in the following examples.

set(prolog_style_variables).
clear(print_kept).
assign(max_given, 300).

If, however, we make the declarations (the precedences are irrelevant)

op(100, fx, set).
op(100, fx, clear).
op(100, xfx, assign).

then we may write

set prolog_style_variables.
clear print_kept.
max_given assign 300.

106APPENDIX A. SYNTAX OF FORMULAS AND CLAUSES IN SCAN

List of Figures

4.1 The basic Scan algorithm . . . . . . . . . . . . . . . . . . . . 30 4.2 The extended Scan algorithm . . . . . . . . . . . . . . . . . . 40 4.3 A model for XScan . . . . . . . . . . . . . . . . . . . . . . . 42 4.4 Visualization of a deduction state . . . . . . . . . . . . . . . . 44

5.1 The algorithm Consistency . . . . . . . . . . . . . . . . . . 57 5.2 The algorithm Linearity . . . . . . . . . . . . . . . . . . . . 63 5.3 The algorithm Unskolemize . . . . . . . . . . . . . . . . . . 65

6.1 The basic algorithm of Scan . . . . . . . . . . . . . . . . . . 76 6.2 The redundancy check of Scan . . . . . . . . . . . . . . . . . 77 6.3 Purification of literals . . . . . . . . . . . . . . . . . . . . . . 78 6.4 Preprocessing of generated clauses . . . . . . . . . . . . . . . 79 6.5 Postprocessing of generated clauses . . . . . . . . . . . . . . . 80 6.6 Scan inference rules . . . . . . . . . . . . . . . . . . . . . . . 86 6.7 Scan resource control options . . . . . . . . . . . . . . . . . . 87 6.8 Scan output parameters . . . . . . . . . . . . . . . . . . . . . 88 6.9 Indexing options . . . . . . . . . . . . . . . . . . . . . . . . . 89 6.10 Otter’s inference process . . . . . . . . . . . . . . . . . . . . 91

Bibliography

[Ack35a] Wilhelm Ackermann. Untersuchung über das Eliminationsproblem der mathematischen Logik. Mathematische Annalen, 110:390– 413, 1935.

[Ack35b] Wilhelm Ackermann. Zum Eliminationsproblem der mathematischen Logik. Mathematische Annalen, 111:61–63, 1935.

[BS71] John Bell and Alan Slomson. Models and Ultraproducts. North Holland, 1971.

[Fra55] R. Fraissé. Sur quelques classifications des relations, basée sur des isomorphismes restreints. Ann. Sci. Ećole Sup., 71:363–388, 1955.

[GO92] D. Gabbay and H.J. Ohlbach. Quantifier elimination in secondorder predicate logic. In Proceedings of the KR’92, Principle of Knowledge Representation and Reasoning, pages 425–436. Morgan Kaufmann (1992), 1992.

[Göd30] Kurt Gödel. Über die Vollständigkeit des Logikkalküls. PhD thesis, University of Vienna, 1930.

[Hen61] L. Henkin. Some remarks on infinitely long formulas. In Infinitistic Methods, pages 167–183. Pergamon Press, Oxford, 1961.

[HET84] J. Flum H. Ebbinghaus and W. Thomas. Mathematical Logic. Springer, 1984.

[Hod84] Wilfried Hodges. Elementary predicate logic. In Gabbay Dov M and Franz Guenthner, editors, Handbook of Philosophical Logic, Vol. I, Elements of Classical Logic, Synthese Library Vol. 164, pages 2–131. D. Reidel Publishing Company, Dordrecht, 1984.

[Kei71] H.J. Keisler. Model theory for infinitary logic. North Holland, 1971.

[Kow75] Robert Kowalski. A proof procedure using connection graphs. Journal of the ACM, 22(4):572–595, October 1975.

[Lin69] P. Lindström. On extensions of elementary logic. Theoria, 35, 1969.

[McC88] William W. McCune. Unskolemizing clause sets. Information Processing Letters, 29:257–263, 1988.

[McC90] William McCune. Otter 2.0. In Mark Stickel, editor, Proc. of 10^{th} Internation Conference on Automated Deduction, LNAI 449, pages 663–664. Springer Verlag, 1990.

[NS95] Andreas Nonnengart and Andrzej Szalas. A fixpoint approach to second-order quantifier elimination with applications to correspondence theory. Technical report, Saarbrücken, 1995.

[Rob65] John Alan Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23–41, 1965.

[Sza92] Andrzej Szałas. On correspondence between modal and classical logic: Automated approach. Technical Report MPI–I–92–209, March 1992.

[vB83] Johan van Benthem. Modal Logic and Classical Logic. Bibliopolis, Naples, 1983.

[vB84] Johan van Benthem. Correspondence theory. In Gabbay Dov M and Franz Guenthner, editors, Handbook of Philosophical Logic, Vol. II, Extensions of Classical Logic, Synthese Library Vol. 165, pages 167–248. D. Reidel Publishing Company, Dordrecht, 1984.

[vBD84] Johan van Benthem and Kees Doets. Higher-order logic. In Dov Gabbay and Franz Guenthner, editors, Handbook of Philosophical Logic, Vol. I, Elements of Classical Logic, Synthese Library Vol. 164, pages 275–329. D. Reidel Publishing Company, Dordrecht,