Circumscription: A Reduction Algorithm

Patrick Doherty, Witold Łukaszewicz, Andrzej Szałas, Computing Circumscription Revisited: A Reduction Algorithm, Journal of Automated Reasoning, Dec. 1995

Definitions

Definition 1 (Second-Order Circumscription) Let P be a tuple of distinct predicate constants, S be a tuple of distinct function and/or predicate constants disjoint from P, and let T (P , S) be a sentence. The second-order circumscription of P in T (P , S) with variable S, written Circ_{SO}(T; P; S), is the sentence

T (P , S) ∧ ∀Φ Ψ .¬ [T (Φ , Ψ ) ∧ Φ < P] (1)

where Φ and Ψ are tuples of variables similar to P and S, respectively.

(1) can be rewritten as

T (P , S) ∧ ∀Φ Ψ .[T (Φ , Ψ ) ∧ [Φ ≤ P]] ⊃ [P ≤ Φ ]].

We consider only the second-order part of the above formula, i.e.

∀Φ Ψ .[T (Φ , Ψ ) ∧ [Φ ≤ P]] ⊃ [P ≤ Φ ]].

Definition 2 A predicate variable Φ occurs positively (resp. negatively) in a formula A if conjunctive normal form of A contains a subformula of the form Φ(t̄) (resp. ¬Φ(t̄)). A formula A is said to be positive (resp. negative) w.r.t. Φ iff all occurrences of Φ in A are positive (resp. negative).

Definition 3 A first-order sentence T is said to be existential (universal) iff it is of the form ∃x. T_{1} (or ∀x. T_{1}, respectively), where T_{1} is quantifier free.

Definition 4 Let ϕ be either a predicate constant or a predicate variable and ϕ be a tuple of predicate constants or a tuple of predicate variables. Then

• a formula T (ϕ) is said to be separated w.r.t. ϕ iff it is of the form T_{1}(ϕ)∧T_{2}(ϕ) where T_{1}(ϕ) is positive w.r.t. ϕ and T_{2} is negative w.r.t. ϕ

• a sentence T is said to be separable w.r.t. ϕ iff T is equivalent to a formula of the form

m ; ⋁ ; i=1 [B_{i}(ϕ) ∧ (U_{i} ≤ ϕ)] (2)

where B_{i}(ϕ) is a formula containing no positive occurrences of predicate constants (variables) from ϕ and each U_{i} is an n-tuple of predicate expressions not containing predicate constants (variables) of ϕ.

Useful tautologies

Proposition 1 The following pairs of formulas are equivalent.

Here Q stands for any quantifier A, B, C are formulas such that C does not contain free occurrence of a variable x. In clauses (15) and (16), t̄, t̄_{1}, …, t̄_{n} are n-tuples of terms and it is assumed that neither C nor any term from t̄, t̄_{1}, …, t̄_{n} contains variables from x̄. In clause (17), f is a function variable which does not occur in A.

(1) ¬¬A  and A
(2) ¬(A∧B)  and ¬A∨¬B
(3) ¬(A∨B)  and ¬A∧¬B
(4) ¬∀xA(x)  and ∃x¬A(x)
(5) ¬∃xA(x)  and ∀x¬A(x)
(6) ∃x(A(x)∨B(x))  and ∃xA(x)∨∃xB(x)
(7) ∀x(A(x)∧B(x))  and ∀xA(x)∧∀xB(x)
(8) Qx(A(x))∧C  and Qx(A(x)∧C)
(9) C∧Qx(A(x))  and Qx(C∧A(x))
(10) Qx(A(x))∨C  and Qx(A(x)∨C)
(11) C∨Qx(A(x))  and Qx(C∨A(x))
(12) QxQyA  and QyQxA
(13) A∧(B∨C)  and (A∧B)∨(A∧C)
(14) (A∨B)∧C  and (A∧C)∨(B∧C)
(15) A(t̄)  and ∀x̄(A(t̄ ← x̄)∨x̄ ≠ t̄)
(16) A(t̄_{1})∨ ⋯ ∨A(t̄_{n}) and ∃x̄(x̄ = t̄_{1}∨ ⋯ ∨x̄ = t̄_{n})∧A(t̄_{1} ← x̄))
(17) ∀x̄∃yA(x̄ …)  and ∃f∀x̄A(x̄, y ← f(x̄), …)
(18) A(t̄_{1})∧ ⋯ ∧A(t̄_{n}) and ∀x̄.(x̄ ≠ t̄_{1}∧ ⋯ ∧x̄ ≠ t̄_{n})∨A(t̄_{1} ← x̄)).

(15) – used by Ackermann.

(16) – generalization of Ackermann’s technique; makes the technique work in the case of clauses containing more than one positive (or negative) occurrence of the eliminated predicate.

(17) – allows to perform Skolemization (i.e. elimination of existential quantifiers) and unskolemization (i.e. elimination of Skolem functions) in such a way that equivalence is preserved. We call this equivalence second-order skolemization.

The elimination algorithm

Based on the following lemma, proved by Ackermann in 1934.

Lemma 1 (Ackermann) Let Φ be a predicate variable and A(x̄), B(Φ) be formulae without second-order quantification. Let B(Φ) be positive w.r.t. Φ and let A contain no occurrences of Φ at all. Then the following equivalences hold:

∃Φ∀x̄[Φ(x̄)∨A(x̄, z̄)]∧B(Φ ← ¬Φ) ≡ B(Φ ← A(x̄, z̄)) (3)

∃Φ∀x̄[¬Φ(x̄)∨A(x̄, z̄)]∧B(Φ) ≡ B(Φ ← A(x̄, z̄)) (4)

where in the righthand formulae the arguments x̄ of A are each time substituted by the respective actual arguments of Φ (renaming the bound variables whenever necessary).

Proposition 2 Let A be a formula of the form pref(A_{1}∧ ⋯ ∧A_{q}), where pref is a prefix of first-order quantifiers and A_{1}, …, A_{q} are disjunctions of literals. In addition, let Φ be a predicate variable occuring in A and Conj(A) be those conjuncts in A where ϕ occurs. Assume that for any conjunct in Conj(A), Φ occurs either positively, or both positively and negatively (or analogously, negatively, or both negatively and positively). Then

∃ΦA ≡ pref(A_{i_{1}}∧ ⋯ ∧A_{i_{r}}) (5)

where i_{1}, …, i_{r} ∈ {1, …, q} and A_{i_{1}}, …, A_{i_{r}} are all the conjuncts that do not contain occurrences of Φ (the empty conjunction is regarded to be equivalent to T).

The algorithm

Input: a formula of the form ∃Φ.A, where A is a first-order formula Output: its first-order equivalent or failure^{∗}.

The algorithm can also be used for formulae of the form ∀Φ.A, since it is equivalent to ¬∃Φ.¬A. Thus, by repeating the algorithm one can deal with formulae containing arbitrarily many second-order quantifiers.

∗The failure of the algorithm does not mean that the second-order formula at hand cannot be reduced to its first-order equivalent. The problem we are dealing with is not even partially decidable.

The algorithm consists of three basic phases:

1. preprocessing;

2. preparation for Ackermann’s lemma;

3. application of Ackermann’s lemma.

It is always assumed that (1) whenever the goal specific for a current phase is reached, then the remaining steps of the phase are skipped, (2) every time the equivalence (5) of Proposition 2 is applicable, it should be applied.

Preprocessing

The purpose of this phase is to transform the formula ∃Φ.A into a form that separates positive and negative occurrences of the quantified predicate variable Φ. The form we want to obtain is^{∗}

∃x̄∃Φ[(A_{1}(Φ)∧B_{1}(Φ))∨ ⋯ ∨(A_{n}(Φ)∧B_{n}(Φ))], (6)

where, for each 1 ≤ i ≤ n, A_{i}(Φ) is positive w.r.t. Φ and B_{i}(Φ) is negative w.r.t. Φ.^{†}

To achieve the goal of this phase, apply the steps below in the following order.

∗It should be emphasized that not every formula is reducible into this form. †To increase the strength of the algorithm, it is essential to move as many existentially quantified variables as possible into the prefix of (6).

1. Eliminate the connectives ⊃ and ≡ using the usual definitions. Remove redundant quantifiers. Rename individual variables until all quantified variables are different and no variable is both bound and free. Using the usual equivalences, move the negation connective to the right until all its occurrences immediately proceed atomic formulae.

2. Move universal quantifiers to the right and existential quantifiers to the left applying as long as possible the following equivalences (below Q ∈ {∀, ∃}, ∘ ∈ {∨, ∧} and B contains no occurrences of variables x̄):

• Qx̄(A(x̄) ∘ B) ≡ (Qx̄A(x̄)) ∘ B

• Qx̄(B ∘ A(x̄)) ≡ B ∘ Qx̄A(x̄).

3. Move to the right the existential quantifiers that are in the scope of univeral quantifiers using the equivalences of step 2.

4. Repeat (2) and (3) as long as no new existentially quantified variable can be moved into the prefix.

5. In the matrix of the formula obtained so far, distribute all top-level conjunctions over the disjunctions that occur among their conjuncts. For this purpose, apply the following equivalences:

• A∧(B∨C) ≡ (A∧B)∨(A∧C)

• (A∨B)∧C ≡ (A∧C)∨(B∧C)

If the resulting formula is not in the form (6), then report the failure of the algorithm. Otherwise replace (6) by its equivalent given by

∃x̄(∃Φ(A_{1}(Φ)∧B_{1}(Φ))∨ ⋯ ∨∃Φ.(A_{n}(Φ)∧B_{n}(Φ))). (7)

For each disjunct ∃Φ(A_{i}(Φ)∧B_{i}(Φ)) of (7) try to find its first-order equivalent by performing the next phases to the formula ∃Φ(A_{i}(Φ)∧B_{i}(Φ)). If all the equivalents are obtained, return their disjunction, preceded by the prefix ∃x̄, as the output of the algorithm.

The following example illustrates the described phase. Example 1 Consider the formula ∃Φ[∀x∃y(P (y)∨∃t(Φ(t)∨P (x)∨R(x, t)))∧∃zΦ(z)∧∃u¬Φ(u)]. The following lines show the subsequent transformations.

∃Φ[∀x∃y(P (y)∨∃t(Φ(t)∨P (x)∨R(x, t)))∧∃zΦ(z)∧∃u¬Φ(u)]  ≡ (by 2)
∃zu∃Φ[∀x∃y(P (y)∨∃t(Φ(t)∨P (x)∨R(x, t)))∧Φ(z)∧¬Φ(u)]  ≡ (by 3)
∃zu∃Φ[∀x(∃yP (y)∨∃t(Φ(t)∨P (x)∨R(x, t)))∧Φ(z)∧¬Φ(u)]  ≡ (by 2)
∃zu∃Φ[(∃yP (y)∨∀x∃t(Φ(t)∨P (x)∨R(x, t)))∧Φ(z)∧¬Φ(u)]  ≡ (by 2)
∃zuy∃Φ[(P (y)∨∀x∃t(Φ(t)∨P (x)∨R(x, t)))∧Φ(z)∧¬Φ(u)]  ≡ (by 5)

∃zuy∃Φ[(P (y)∧Φ(z)∧¬Φ(u))∨(∀x∃t(Φ(t)∨P (x)∨R(x, t))∧Φ(z)∧¬Φ(u))] Preparation for Ackermann’s lemma

The goal of this phase is to transform a formula of the form ∃Φ(A(Φ)∧B(Φ)), where A(Φ) (resp. B(Φ)) is positive (resp. negative) w.r.t. Φ, into one of the forms (3) or (4) given in Lemma 1. Both forms can always be obtained and both transformations should be performed because none, one or both forms may require Skolemization. Unskolemization, which occurs in the next phase, could fail in one form, but not in the other. In addition, one form may be substantially smaller than the other. The steps of this phase are based on equivalences (13) – (17) from Proposition 1. Due to the symmetry of Ackermann’s lemma, the steps stated below describe only one of those transformations, namely that leading to the form (3).

1. Transform A(Φ) into the form

pref[(Φ(t̄_{11} )∨ ⋯ ∨Φ(t̄_{1n_{1}} )∨C_{1})∧ ⋯ ∧(Φ(t̄_{k1})∨ ⋯ ∨Φ(t̄_{kn_{k}})∨C_{k})∧D],

where pref is a prefix of first-order quantifiers and Φ does not occur in C_{1}, …, C_{k}, D. This step is always possible by applying the usual technique of obtaining CNF.

2. Transform each conjunct in Step 1. of the form (Φ(t̄_{i1})∨ ⋯ ∨Φ(t̄_{in_{i}})∨C_{i}), where n_{i} > 1, into its equivalent

∃x̄_{i}(∀ȳ(Φ(ȳ)∨x̄_{i} ≠ ȳ∨C_{i})∧(x̄_{i} = t̄_{i1}∨ ⋯ ∨x̄_{i} = t̄_{in_{i}}∨C_{i})

and move all existential quantifiers into the prefix pref.^{∗} Move each of the second conjuncts, (x̄_{i} = t̄_{i1}∨ ⋯ ∨x̄_{i} = t̄_{in_{i}}∨C_{i}), into D and rename it D′.

∗This step is justified by equivalence (16) and (15) of Proposition 1.

3. Transform each conjunct in Step 1 of the form (Φ(t̄_{i1}∨C_{i}) (case n_{i} = 1) into its equivalent ∀ȳ(Φ(ȳ)∨ȳ ≠ t̄_{i1}∨C_{i})

4. Remove all existential quantifiers from the prefix pref using the equivalence of Skolem given by

∀x̄.∃y.A(x̄, y, …) ≡ ∃f.∀x̄.A(x̄, y ← f(x̄), …), (8)

where f is a new function variable. After this transformation the input formula takes the form

∃f̄∃Φpref′[∀ȳ(Φ(ȳ)∨x̄_{1} ≠ ȳ∨C_{1})∧ ⋯ ∧∀ȳ(Φ(ȳ)∨x̄_{k} ≠ ȳ∨C_{k})∧E],(9)

where f̄ is the tuple of the introduced Skolem functions and pref′ contains only universal quantifiers and E is D′∧B(Φ).

5. Transform (9) into its equivalent given by ∃f̄∃Φ∀ȳ[Φ(ȳ)∨pref′((x̄_{1} ≠ ȳ∨C_{1})∧ ⋯ ∧(x̄_{k} ≠ ȳ∨C_{k}))∧pref′E.(10)

Example 1 [continued] There are two formulae to be considered in this phase, namely ∃Φ(P (y)∧Φ(z)∧¬Φ(u)) and ∃Φ∀x∃t(Φ(t)∨P (x)∨R(x, t))∧Φ(z)∧¬Φ(u). We apply phase 2 to the former of the above formulae.

∃Φ(P (y)∧Φ(z)∧¬Φ(u))  ≡ (by 3)

∃Φ(P (y)∧∀r(Φ(r)∨z ≠ r)∧¬Φ(u))

Applying phase 2 to the second formula proceeds as follows.

∃Φ∀x∃t(Φ(t)∨P (x)∨R(x, t))∧Φ(z)∧¬Φ(u)  ≡ (by 3)
∃Φ∀x∃t∀r(Φ(r)∨r ≠ t∨P (x)∨R(x, t))∧∀r(Φ(r)∨z ≠ r)∧¬Φ(u)  ≡ (by 4)

∃f∃Φ∀x∀r(Φ(r)∨r ≠ f(x)∨P (x)∨R(x, f(x)))∧∀r(Φ(r)∨z ≠ r)∧¬Φ(u)

≡ (by 5)

∃f∃Φ∀r[Φ(r)∨(∀x(r ≠ f(x)∨P (x)∨R(x, f(x)))∧z ≠ r)]∧¬Φ(u)

Application of Ackermann’s lemma

The goal of this phase is to eliminate the second-order quantification over Φ, applying Ackermann’s lemma, and then to unskolemize the introduced function variables (by (17) from Proposition 1). The phase consists of the following two steps.

1. Apply Ackermann’s lemma to the formula (10). The resulting formula is of the form

∃f̄[prefE(¬Φ ← pref((x̄_{1} ≠ ȳ∨C_{1})∧ ⋯ ∧(x̄_{k} ≠ ȳ∨C_{k})))]

2. Try to remove all existential quantifiers over function variables using the equivalence (8). If both transformations mentioned in the beginning of phase 2 failed, report failure of the algorithm; otherwise try the remaining possibility.

Simplification.

The formula obtained after phase 3 can often be simplified using Proposition 1 (15) or its generalization (18) in the left to right direction.

Example 1 [continued] We apply phase 3 for the pair of formulae obtained as the result of phase 2.

\begin{matrix}∃Φ(P (y)∧∀r(Φ(r)∨z ≠ r)∧¬Φ(u)) & ≡ & (by 1) \\ P (y)∧z ≠ u. \end{matrix}

∃f∃Φ∀r[Φ(r)∨(∀x(r ≠ f(x)∨P (x)∨R(x, f(x)))∧z ≠ r)]∧¬Φ(u)

≡ (by 1)
∃f∀x(u ≠ f(x)∨P (x)∨R(x, f(x)))∧z ≠ u  ≡ (by 2)

∀x∃t(u ≠ t∨P (x)∨R(x, t))∧z ≠ u.

Collecting the above results, we get the first-order equivalent of the input formula, namely ∃zuy(P (y)∧z ≠ u∨∀x∃t(u ≠ t∨P (x)∨R(x, t))∧z ≠ u).

Discussion of the algorithm Assume that a second-order formula A is of the form

∃Φ.[(prefB)∧(pref′C)], (11) where,

• pref and pref′ are sequences of first-order quantifiers,

• B and C are quantifier-free formulae in conjunctive normal forms,

• B is positive w.r.t. Φ, and

• C is negative w.r.t. Φ.

The following proposition holds.

Proposition 3 Let A be an input formula of the form (11). Then, as a result, the algorithm returns a first-order formula provided that unskolemization (if necessary) succeeds.

Skolem functions are introduced in the second step of the algorithm whenever existential quantifiers are to be eliminated. These can appear in the input formula or may be introduced via application of the equivalence (16) of Proposition 1.

In the following proposition, we formulate conditions under which no Skolem functions are introduced and the algorithm terminates successfully.

Proposition 4 If one of the following conditions holds

• B is universal and each conjunct of B contains at most one occurrence of Φ, or

• C is universal and each conjunct of C contains at most one occurrence of ¬Φ,

then the algorithm always returns a first-order formula as output.

If the input formula cannot be transformed into the form (11) then the algorithm fails.

Examples

Example 2 (Block example) Let Γ(Ab, On) be the theory

[b1 ≠ b2∧B(b1)∧B(b2)∧¬On(b1)]
∧[∀x.B(x)∧¬Ab(x) ⊃ On(x)],  (12)

where B and On are abbreviations for Block and Ontable, respectively. The circumscription of Γ(Ab, On) with Ab minimized and On varied is

Circ_{SO}(Γ(Ab, On); Ab; On) ≡
Γ(Ab, On)∧∀Φ∀Ψ[[Γ(Φ, Ψ)∧Φ ≤ Ab] ⊃ [Ab ≤ Φ]],  (13)

where

Γ(Φ, Ψ) ≡  [b1 ≠ b2∧B(b1)∧B(b2)∧¬Ψ(b1)]
∧[∀x.B(x)∧¬Φ(x) ⊃ Ψ(x)]  (14)
Φ ≤ Ab ≡  ∀x.Φ(x) ⊃ Ab(x)  (15)
Ab ≤ Φ ≡  ∀x.Ab(x) ⊃ Φ(x).  (16)

In the following, we will reduce

∀Φ∀Ψ[Γ(Φ, Ψ)∧[Φ ≤ Ab] ⊃ [Ab ≤ Φ]]  (17)

in (13). Negating (17), we get

∃Φ∃Ψ[Γ(Φ, Ψ)∧[Φ ≤ Ab]∧¬[Ab ≤ Φ]].  (18)

Since we will try to remove Φ first, we replace (18) by the equivalent

∃Ψ∃Φ[Γ(Φ, Ψ)∧[Φ ≤ Ab]∧¬[Ab ≤ Φ]].  (19)

Preprocessing. Replacing Γ(Φ, Ψ), Φ ≤ Ab and Ab ≤ Φ by their equivalent forms (14)–(16), eliminating ⊃ and renaming individual variables, we obtain

∃Ψ∃Φ[b1 ≠ b2∧B(b1)∧B(b2)∧¬Ψ(b1)
∧∀x(¬B(x)∨Φ(x)∨Ψ(x))
∧∀y(¬Φ(y)∨Ab(y))∧∃z(Ab(z)∧¬Φ(z))].  (20)

We next move ∃z to the left, obtaining

∃z∃Ψ∃Φ[b1 ≠ b2∧B(b1)∧B(b2)∧¬Ψ(b1)
∧∀x(¬B(x)∨Φ(x)∨Ψ(x))
∧∀y(¬Φ(y)∨Ab(y))∧(Ab(z)∧¬Φ(z))].  (21)

1 Preparation for Ackermann’s lemma. (21) is in the form suitable for application of Ackermann’s lemma. To make this more explicit, we rewrite (21) as

∃z∃Ψ∃Φ∀x[(Φ(x)∨¬B(x)∨Ψ(x))
∧∀y(¬Φ(y)∨Ab(y))∧¬Φ(z)∧Ab(z)
∧¬Ψ(b1)∧b1 ≠ b2∧B(b1)∧B(b2)].  (22)

Application of Ackermann’s lemma. Applying Ackermann’s lemma to (22), we obtain

∃z∃Ψ[∀y(¬B(y)∨Ψ(y)∨Ab(y))
∧(¬B(z)∨Ψ(z))∧Ab(z)
∧¬Ψ(b1)∧b1 ≠ b2∧B(b1)∧B(b2)].  (23)

We next try to remove Ψ in (23). Preprocessing. The formula (23) is already in the form which is the goal of this phase. To see this, we rewrite it as

∃z∃Ψ[¬Ψ(b1)∧∀y(Ψ(y)∨¬B(y)∨Ab(y))
∧(Ψ(z)∨¬B(z))∧Ab(z)∧b1 ≠ b2∧B(b1)∧B(b2)].  (24)

Preparation for Ackermann’s lemma. Applying Proposition 1 (15) to ¬Ψ(b1) in (24), we obtain

∃z∃Ψ∀s[(¬Ψ(s)∨s ≠ b1)∧∀y(Ψ(y)∨¬B(y)∨Ab(y))
∧(Ψ(z)∨¬B(z))∧Ab(z)∧b1 ≠ b2∧B(b1)∧B(b2)].  (25)

Application of Ackermann’s lemma. We apply Ackermann’s lemma to (25), obtaining

∃z∀y[(y ≠ b1∨¬B(y)∨Ab(y))
∧(z ≠ b1∨¬B(z))∧Ab(z)∧b1 ≠ b2∧B(b1)∧B(b2)].  (26)

Let us simplify (26) before negating by using Proposition 1(15). (26) is equivalent to

∃z[(¬B(b1)∨Ab(b1))
∧(z ≠ b1∨¬B(z))∧Ab(z)∧b1 ≠ b2∧B(b1)∧B(b2)].  (27)

Negating and simplifying (27) results in

∀z[(B(b1)∧¬Ab(b1))
∨(z = b1∧B(z)∨¬Ab(z)∨b1 = b2∨¬B(b1)∨¬B(b2)].  (28)

The first-order formula (28) is logically equivalent to the second-order formula (17). Consequently,

Circ_{SO}(Γ(Ab, On); Ab; On) ≡ Γ(Ab, On)∧
∀z[(B(b1)∧¬Ab(b1))
∨(z = b1∧B(z)∨¬Ab(z)∨b1 = b2∨¬B(b1)∨¬B(b2)].  (29)

At this stage, the algorithm terminates but we can continue simplifying relative to the original theory. (28) together with

(12) implies

Ab(b1)→∀z(¬Ab(z)∨(z = b1∧B(z)))  (30)

and thus implies

∀z(Ab(z) ⊃ (z = b1∧B(z))),  (31)

which states that for any object z, either it is normal (¬Ab(z)) or it is a block and b1. In other words, the only abnormal object is the block b1.

Example 3 (Birthday Example) This example contains both existentially quantified and universal formulae. In addition, it contains both unary and binary predicates.

Let Γ(Ab, G) be the theory

[∃x∃y(B(y)∧F (x, y)∧¬G(x, y))]
∧[∀x∀y(B(y)∧F (x, y)∧¬Ab(x, y) ⊃ G(x, y))],  (32)

where B, F and G are abbreviations for Birthday, F riend and Gives − Gift, respectively. Here Ab(x, y) has the following intuitive interpretation: “x behaves abnormally w.r.t. y in the situation when y has a birthday and x is a friend of y”. The circumscription of Γ(Ab, G) with Ab minimized and G varied is

Circ_{SO}(Γ(Ab, G); Ab; G) ≡
Γ(Ab, G)∧∀Φ∀Ψ[Γ(Φ, Ψ)∧[Φ ≤ Ab] ⊃ [Ab ≤ Φ]],  (33)

Γ(Φ, Ψ)  ≡ [∃x∃y(B(y)∧F (x, y)∧¬Ψ(x, y))]∧
[∀x∀y(B(y)∧F (x, y)∧¬Φ(x, y) ⊃ Ψ(x, y))] (34)
Φ ≤ Ab ≡ ∀x∀y[Φ(x, y) ⊃ Ab(x, y)]  (35)
Ab ≤ Φ ≡ ∀x∀y[Ab(x, y) ⊃ Φ(x, y)].  (36)

In the following, we will reduce

∀Φ∀Ψ[Γ(Φ, Ψ)∧[Φ ≤ Ab] ⊃ [Ab ≤ Φ]]  (37)

in (33). Negating (37), we obtain

∃Φ∃Ψ[Γ(Φ, Ψ)∧[Φ ≤ Ab]∧¬[Ab ≤ Φ]].  (38)

We remove Ψ first.

Preprocessing. Replacing Γ(Φ, Ψ), Φ ≤ Ab and Ab ≤ Φ by their equivalents given by (34)–(36), eliminating ⊃, renaming individual variables and moving existential quantifiers over individual variables to the left, we obtain

∃x∃y∃q∃r∃Φ∃Ψ[B(y)∧F (x, y)∧¬Ψ(x, y)
∧∀u∀z(¬B(z)∨¬F (u, z)∨Φ(u, z)∨Ψ(u, z))
∧∀s∀t(¬Φ(s, t)∨Ab(s, t))∧Ab(q, r)∧¬Φ(q, r)].  (39)

Preparation for Ackermann’s lemma. (39) is in the form suitable for application of Ackermann’s lemma. To see this, we rewrite it as

∃x∃y∃q∃r∃Φ∃Ψ∀u∀z[(Ψ(u, z)∨¬B(z)∨¬F (u, z)∨Φ(u, z))
∧¬Ψ(x, y)∧B(y)∧F (x, y)
∧∀s∀t(¬Φ(s, t)∨Ab(s, t))∧Ab(q, r)∧¬Φ(q, r)].  (40)

Application of Ackermann’s lemma. Applying Ackermann’s lemma to (40), we obtain

∃x∃y∃q∃r∃Φ[(¬B(y)∨¬F (x, y)∨Φ(x, y))∧B(y)∧F (x, y)

∧∀s∀t(¬Φ(s, t)∨Ab(s, t))∧Ab(q, r)∧¬Φ(q, r)].  (41)

We now remove Φ in (41). Preprocessing. (41) is in the form which is the goal of this phase. Preparation for Ackermann’s lemma. Using Proposition 1 (15), we replace (41) by

∃x∃y∃q∃r∃Φ∀v∀w[(Φ(v, w)∨v ≠ x∨w ≠ y∨¬B(y)∨¬F (x, y))

∧∀s∀t(¬Φ(s, t)∨Ab(s, t))∧¬Φ(q, r)∧B(y)∧F (x, y)∧Ab(q, r)]. (42)

∃x∃y∃q∃r∀s∀t[(s ≠ x∨t ≠ y∨¬B(y)∨¬F (x, y)∨Ab(s, t))∧

(q ≠ x∨r ≠ y∨¬B(y)∨¬F (x, y))
∧B(y)∧F (x, y)∧Ab(q, r)].  (43)

Before negating, we simplify (43) which results in

∃x∃y∃q∃r[(¬B(y)∨¬F (x, y)∨Ab(x, y))
∧(q ≠ x∨r ≠ y∨¬B(y)∨¬F (x, y))
∧B(y)∧F (x, y)∧Ab(q, r)].  (44)

Negating (44), we obtain

∀x∀y∀q∀r[(B(y)∧F (x, y)∧¬Ab(x, y))∨(q = x∧r = y
∧B(y)∧F (x, y))∨¬B(y)∨¬F (x, y)∨¬Ab(q, r)].  (45)

(45) is logically equivalent to

∀x∀y∀q∀r[¬(B(y)∧F (x, y))∨((B(y)∧F (x, y))

∧(¬Ab(x, y)∨(q = x∧r = y)))∨¬Ab(q, r)],  (46)

which is equivalent to

∀x∀y∀q∀r[¬(B(y)∧F (x, y))∨¬Ab(x, y)
∨(q = x∧r = y)∨¬Ab(q, r)].  (47)

The first-order formula (47) is logically equivalent to the second-order formula (37). Consequently,

Circ_{SO}(Γ(Ab, G); Ab; G) ≡
Γ(Ab, G)∧∀x∀y∀q∀r[¬(B(y)∧F (x, y))∨¬Ab(x, y)
∨(q = x∧r = y)∨¬Ab(q, r)].  (48)

A more informative sentence, equivalent to (47), is

∀x∀y∀q∀r[Ab(x, y)∧Ab(q, r)∧B(y)∧F (x, y) ⊃ (q = x∧r = y)] (49)

(49), together with the theory Γ(Ab, G), states that there is exactly one pair of individuals, x and y, such that y has a birthday, x is a friend of y and x does not give a gift to y.

Example 4 (Hospital Example) Let Γ be the theory

[∀x∃y(Ab(x, y) ⊃ H(x, y))]
∧[∀x∃y(¬Ab(x, y) ⊃ H(x, y))].  (50)

Here H(x, y) and Ab(x, y) are to be intuitively interpreted as “x is in a hospital in a situation y” and “x behaves abnormally in a situation y”, respectively. The circumscumscription of Γ, with Ab minimized and H varied is

Circ_{SO}(Γ; Ab; H) ≡
Γ∧∀Φ∀Ψ[Γ(Φ, Ψ)∧[Φ ≤ Ab] ⊃ [Ab ≤ Φ]],  (51)

where

Γ(Φ, Ψ) ≡  ∀x∃y[Φ(x, y) ⊃ Ψ(x, y)]
∧∀x∃y[¬Φ(x, y) ⊃ Ψ(x, y)]  (52)
Φ ≤ Ab ≡ ∀x∀y[Φ(x, y) ⊃ Ab(x, y)]  (53)
Ab ≤ Φ ≡ ∀x∀y[Ab(x, y) ⊃ Φ(x, y)].  (54)

In the following, we will reduce

∀Φ∀Ψ[Γ(Φ, Ψ)∧[Φ ≤ Ab] ⊃ [Ab ≤ Φ]]  (55)

in (51). Negating (55), we obtain

∃Φ∃Ψ[Γ(Φ, Ψ)∧[Φ ≤ Ab]∧¬[Ab ≤ Φ]].  (56)

Since we will try to remove Φ first, we replace (56) by its equivalent given by

∃Ψ∃Φ[Γ(Φ, Ψ)∧[Φ ≤ Ab]∧¬[Ab ≤ Φ]].  (57)

Preprocessing. Replacing Γ(Φ, Ψ), Φ ≤ Ab and Ab ≤ Φ by their equivalents given by (52)–(54), eliminating ⊃ and renaming individual variables, we obtain

∃Ψ∃Φ[∀x∃y(¬Φ(x, y)∨Ψ(x, y))∧∀q∃r(Φ(q, r)∨Ψ(q, r))
∧∀u∀v(¬Φ(u, v)∨Ab(u, v))∧∃s∃t(Ab(s, t)∧¬Φ(s, t))].  (58)

Moving ∃s∃t to the left and rearranging the resulting formula, we obtain

∃s∃t∃Ψ∃Φ[∀q∃r(Φ(q, r)∨Ψ(q, r))∧∀x∃y(¬Φ(x, y)∨Ψ(x, y))

∧∀u∀v(¬Φ(u, v)∨Ab(u, v))∧Ab(s, t)∧¬Φ(s, t)].  (59)

Preparation for Ackermann’s lemma. Using Proposition 1 (15), we replace Φ(q, r) in (59) by ∀z∀w(Φ(z, w)∨z ≠ q∨w ≠ r). This results in

∃s∃t∃Ψ∃Φ[∀q∃r(∀z∀w(Φ(z, w)∨z ≠ q∨w ≠ r)
∨Ψ(q, r))∧∀x∃y(¬Φ(x, y)∨Ψ(x, y))
∧∀u∀v(¬Φ(u, v)∨Ab(u, v))∧Ab(s, t)∧¬Φ(s, t)]  (60)

which is equivalent to

∃s∃t∃Ψ∃Φ[∀q∃r∀z∀w(Φ(z, w)∨z ≠ q∨w ≠ r∨Ψ(q, r))
∧∀x∃y(¬Φ(x, y)∨Ψ(x, y))
∧∀u∀v(¬Φ(u, v)∨Ab(u, v))∧Ab(s, t)∧¬Φ(s, t)].  (61)

We next eliminate ∃r by Skolemization and move ∀q to the right and ∀z∀w to the left. The resulting formula is (below f is the introduced function variable)

∃s∃t∃Ψ∃f∃Φ∀z∀w[(Φ(z, w)∨∀q(z ≠ q∨w ≠ f(q)
∨Ψ(q, f(q))))∧∀x∃y(¬Φ(x, y)∨Ψ(x, y))
∧∀u∀v(¬Φ(u, v)∨Ab(u, v))∧Ab(s, t)∧¬Φ(s, t)].  (62)

Application of Ackermann’s lemma. Applying Ackermann’s lemma to (62), we obtain

∃s∃t∃f∃Ψ[∀x∃y(∀q(x ≠ q∨y ≠ f(q)∨Ψ(q, f(q)))∨Ψ(x, y))

∧∀u∀v(∀q(u ≠ q∨v ≠ f(q)∨Ψ(q, f(q)))∨Ab(u, v))
∧Ab(s, t)∧∀q(s ≠ q∨t ≠ f(q)∨Ψ(q, f(q)))]  (63)

which is equivalent to

∃s∃t∃f∃Ψ∀x∃y∀q∀u∀v[(x ≠ q∨y ≠ f(q)∨Ψ(q, f(q))∨Ψ(x, y))
∧(u ≠ q∨v ≠ f(q)∨Ψ(q, f(q))∨Ab(u, v))
∧Ab(s, t)∧(s ≠ q∨t ≠ f(q)∨Ψ(q, f(q)))].  (64)

Since all occurrences of Ψ in each conjunct in (64) are positive, all the conjuncts including Ψ, together with ∃Ψ, can be removed by Proposition 2. This yields

∃s∃t∃f∃Ψ∀x∃y∀q∀u∀v.Ab(s, t)  (65)

which reduces to

∃s∃t.Ab(s, t).  (66)

Since we negated the original formula before applying the algorithm, we now negate the result, obtaining

∀s∀t.¬Ab(s, t).  (67)

The first-order formula (67) is logically equivalent to the second-order formula (55). Consequently,

Circ_{SO}(Γ; Ab; H) ≡ Γ∧∀s∀t.¬Ab(s, t).  (68)

which implies

∀x∃yH(x, y).  (69)

This is a variant of an example from Reiter. Rather than using the function city as Reiter does, we will use a relation C(x, y) with suitable axioms.

Example 5 (Vancouver Example) We begin by defining the binary relation C with the intention that C(x, y) holds iff the city of x is y. In our axiomatization, Reiter’s axiom,

∀x.¬Ab(x) ⊃ city(x) = city(wife(x))  (70)

is replaced with

∀x∀y∀z.¬Ab(x)∧C(x, y)∧C(wife(x), z) ⊃ y = z.  (71)

In addition, we add the following axiom guaranteeing that C represents a function:

∀x∀y∀z.C(x, y)∧C(x, z) ⊃ y = z.  (72)

We do not require that all people live in cities, i.e. we reject the axiom

∀x∃y.C(x, y).  (73)

So, the distinction is that our representation of the city function is partial, whereas Reiter’s is total. Intuitively, our choice seems to make more sense.

Let Γ(Ab, C) be the theory

[∀x∀y∀z.¬Ab(x)∧C(x, y)∧C(wife(x), z) ⊃ y = z]

(74)

The circumscription of Γ(Ab, City) with Ab minimized and C varied is

Circ_{SO}(Γ(Ab, C); Ab; C) ≡
Γ(Ab, C)∧∀Φ∀Ψ[Γ(Φ, Ψ)∧[Φ ≤ Ab] ⊃ [Ab ≤ Φ],  (75)

where

Γ(Φ, Ψ)  ≡ [∀x∀y∀z.¬Φ(x)∧Ψ(x, y)∧Ψ(wife(x), z) ⊃ y = z]
∧[∀x∀y∀z.Ψ(x, y)∧Ψ(x, z) ⊃ y = z].  (76)
Φ ≤ Ab ≡ ∀x.Φ(x) ⊃ Ab(x)  (77)
Ab ≤ Φ ≡ ∀x.Ab(x) ⊃ Φ(x).  (78)

In the following, we will reduce

∀Φ∀Ψ[Γ(Φ, Ψ)∧[Φ ≤ Ab] ⊃ [Ab ≤ Φ]]  (79)

in (75). Negating (79), we obtain

∃Φ∃Ψ[Γ(Φ, Ψ)∧[Φ ≤ Ab]∧¬[Ab ≤ Φ]].  (80)

We start by removing Ψ.

Preprocessing. Replacing Γ(Φ, Ψ), Φ ≤ Ab and Ab ≤ Φ by their equivalents given by (76)–(78), eliminating ⊃ and renaming individual variables, we obtain

∃Φ∃Ψ[∀x∀y∀z(Φ(x)∨¬Ψ(x, y)∨¬Ψ(wife(x), z)∨y = z)∧

∀u∀v∀w(¬Ψ(u, v)∨¬Ψ(u, w)∨v = w))∧
∀s(¬Φ(s)∨Ab(s))∧∃t(Ab(t)∧¬Φ(t))].  (81)

Note that Ψ can be removed directly using Proposition 2, since all instances of Ψ occurring in (81) are negative. To prepare the latter formula into the form suitable for the application of Proposition 2, we move all quantifiers ranging over individual variables to the left. This results in

∃Φ∃Ψ∀x∀y∀z∀u∀v∀w∀s∃t[(Φ(x)∨¬Ψ(x, y)
∨¬Ψ(wife(x), z)∨y = z)
∧(¬Ψ(u, v)∨¬Ψ(u, w)∨v = w)
∧(¬Φ(s)∨Ab(s))∧Ab(t)∧¬Φ(t)].  (82)

Applying Proposition 2 to (82), we obtain

∃Φ∀x∀y∀z∀u∀v∀w∀s∃t[(¬Φ(s)∨Ab(s))∧Ab(t)∧¬Φ(t)]  (83)

which reduces to

∃Φ∀s∃t[(¬Φ(s)∨Ab(s))∧Ab(t)∧¬Φ(t).  (84)

We next try to remove Φ. Again, this can be done directly using Proposition 2, since all instances of Φ in (84) are negative. This results in

∀s∃t.Ab(t)  (85)

which is equivalent to

∃t.Ab(t).  (86)

Taking the negation of (86) results in

∀t.¬Ab(t).  (87)

The first-order formula (87) is logically equivalent to the second-order formula (79). Consequently,

Circ_{SO}(Γ; Ab; C) ≡ Γ∧∀t¬Ab(t).  (88)

Remarks on the algorithm

• The algorithm always terminates and is sound, i.e. the output first-order formula, if obtained, is equivalent to the input second-order formula.

• There are two reasons causing the failure of the algorithm: (1) impossibility of separating positive and negative occurrences of the predicate variable Φ during the preprocessing phase; (2) the impossibility of unskolemization during the third phase.

• Although the algorithm may seem a bit complex, the calculations it describes may be performed without any computer support.

• For the sake of clarity the algorithm is not presented in its most efficient form. The possible directions of its optimization follow from the examples presented throught the paper.

• Observe that one usually deals with the elimination problem over a first-order definable class of models. In such a case it is sometimes possible to simplify considerably the input formula before running the algorithm. Such a possibility can be considered as an additional heuristics in the preprocessing phase.

Algorithm has been implemented at Linköping University and may be used on line.

http://www.ida.liu.se/labs/kplab/projects/dls/