Artificial Intelligence, 54:397–410, 1992.

An Efficient Method for Eliminating Varying Predicates from a Circumscription

Marco Cadoli^{∗}

Dipartimento di Informatica e Sistemistica,

Università di Roma “La Sapienza”

Thomas Eiter, Georg Gottlob^{†}

Christian Doppler Labor für Expertensysteme,

Institut für Informationssysteme, Technische Universität Wien

Abstract

Circumscription appears to be the most powerful and well-studied technique used in formalizing common-sense reasoning. The general form of predicate circumscription allows for fixed and varying (floating) predicates. We show that the inference problem under this form of circumscription is efficiently reducible to inferencing under circumscription without varying predicates. In fact, we transform this problem even into circumscription without fixed and varying predicates, that is where all predicates are minimized. Thus any theorem prover or algorithm for inferencing under circumscription without fixed and varying predicates is able to handle inferencing under the general form of predicate circumscription. As a consequence, algorithms that compute circumscription for an inference task can be simplified.

∗Mailing address: Via Salaria 113, I-00198 Roma, Italia. E-mail: cadoli@vaxrma.infn.it †Mailing address: Paniglgasse 16, A-1040 Wien, Austria.

Internet e-mail: {eiter,gottlob}@vexpert.dbai.tuwien.ac.at

1 Introduction

Circumscription is a powerful non-monotonic technique that allows us to deal with the representation of incomplete information in knowledge bases. The basic idea of circumscription is to represent implicitly an assumption of normality through the minimization of the extension of predicates formalizing abnormality in a first-order formula. For example, we know that birds normally fly, but exceptions to this general rule can arise. The circumscriptive approach translates this general rule into the formula ∀x.bird(x) ∧ ¬abnormal(x) ⊃ flies(x) and considers only those models of the formula in which the extension of the predicate abnormal is minimal, that is cannot be reduced without leading to an inconsistent interpretation.

The original definition of circumscription by McCarthy [12] did not take into account the possibility of varying the extension of predicates. Variability of predicates means that the extensions of some predicates (the varying ones) can be affected in any way (enlarged or reduced) in order to decrease the extensions of those predicates that are minimized. Etherington, Mercer and Reiter [3] noticed that with the original definition it is impossible to derive new positive facts from a knowledge base. For example, it is impossible to infer flies(T weety) from the fact bird(T weety) and the rule ∀x.bird(x) ∧ ¬abnormal(x) ⊃ flies(x) minimizing abnormal while bird and flies are fixed.

A revised definition of circumscription has been provided by McCarthy in [13], which allows the extensions of some of the predicates to vary, while the extensions of other predicates are minimized. With this new definition of circumscription it is possible to infer new positive facts. If we allow in the previous example the predicate flies to vary, then we can infer flies(T weety). Recently, several theorem provers and inference algorithms for circumscription have been designed [1, 7, 15].

Generally, the set of the predicates of a formula to be circumscribed is partitioned into three subsets: The predicates to be minimized (denoted by P), those that are allowed to vary (denoted by Z) and those whose extension should remain fixed (denoted by Q). Fixed predicates are used to model definite entities that we do not want to be altered by circumscription. More general formulations of circumscription allow arbitrary expressions E(P, x) to be minimized [13] or functions to be varied [10, 11]. These extensions are inessential, cf. Etherington [4, p.132,Theorem 6.3] and de Kleer and Konolige [2], however, and will be disregarded in this paper.

Several authors have addressed the question of simplifying the definition of circumscription, in particular by providing equivalent formulations of predicate circumscription in terms of simpler forms of circumscription. de Kleer and Konolige [2] show that it is possible to translate any first-order formula T into another first-order formula T′ such that the circumscription of T with fixed predicates is equivalent to the circumscription of T′ without fixed predicates. Lifschitz [10] performed a similar transformation for the elimination of varying predicates, but introduced second-order formulae. Yuan and Wang [20] defined a method for eliminating the varying predicates without introducing second-order formulae. The two major drawbacks of their method are that it is incomplete and that it yields in general an exponential-size formula.

In this paper we are concerned with inferring formulae from a circumscription rather than transforming a circumscription into an equivalent one. In particular we exhibit an efficient method for reducing the problem of inference of a formula under circumscription with varying predicates to the problem of inferencing a formula under circumscription where all predicates are minimized.

In this way we show that any algorithm for performing inference under circumscription without varying predicates (for instance the method of Bossu and Siegel [1]) can be used to perform any inference under circumscription with fixed and varying predicates. Since fixed and varying predicates can be bypassed efficiently combining the method in [2] and our method, well-known algorithms for inference under predicate circumscription (for example Przymusinski’s MILO-resolution [15]) can be noticeably simplified.

2 The Reduction

In this section we exhibit a transformation of a pair of first-order formulae T and F into a first-order formula Γ(T ; F; P; Z) such that F follows from the circumscription of T where the P predicates are minimized and the Z predicates vary if and only if ¬u follows from the circumscription of Γ(T ; F; P; Z) under minimization of all predicates, where u is a new 0-ary predicate symbol not occurring in T or F.

We introduce some notation first. In the following, predicate constants and predicate variables are both referred to as predicate symbols. If A denotes a list a_{1}, …, a_{n} of predicate symbols occurring in a formula G, then A′ and A′′ denote the lists a′_{1}, …, a′_{n} and a′′_{1}, …, a′′_{n}, respectively, where it is assumed that for 1 ≤ i ≤ n, a′_{i} and a′′_{i} are new distinct predicate symbols not occurring in G such that a_{i}, a′_{i}, a′′_{i} are of the same arity. AB denotes the concatenation of lists A and B of predicate symbols. If A, B are the respective lists a_{1}, …, a_{n} and b_{1}, …, b_{n} of predicate symbols where a_{i} and b_{i} are of the same arity, 1 ≤ i ≤ n, we use the following notation:

(A ≡ ¬B) stands for ⋀_{1≤i≤n}(∀x_{i}.a_{i}(x_{i}) ≡ ¬b_{i}(x_{i})),

(A < B) stands for [ ⋀_{1≤i≤n}(∀x_{i}.a_{i}(x_{i}) ⊃ b_{i}(x_{i}))] ∧ [ ⋁_{1≤i≤n}(∃x_{i}.¬a_{i}(x_{i}) ∧ b_{i}(x_{i}))],

(A ≡ true) stands for [ ⋀_{1≤i≤n}(∀x_{i}.a_{i}(x_{i}))].

We follow Lifschitz’s well-known notion of parallel circumscription in [10]. For the definition of second order structures and models see [10]; as Lifschitz, we denote the universe of a structure M by |M|. For each list A of predicate constants, we denote by [[ A]]_{M} the extension of the A-predicates in structure M. We write [[ A]]_{M} ≤ [[ A]]_{M′} if and only if for each a in A the extension of a in M is a subset of the extension of a in M′; [[ A]]_{M} < [[ A]]_{M′} means [[ A]]_{M} ≤ [[ A]]_{M′} and [[ A]]_{M} ≠ [[ A]]_{M′}. We write M <_{P;Z} M′ for models M, M′ iff |M| = |M′|, the interpretation of functions and predicates not in P Z is identical and [[ P ]]_{M} < [[ P ]]_{M′}, where P, Z are disjoint lists of predicate constants. Model M is P; Z -minimal iff there is no model M′ such that M′ <_{P;Z} M. If P covers all predicates, minimal means P; ∅-minimal and M < M′ stands for M <_{P;∅} M′. CIRC (T ; P; Z) is defined by the second-order formula

T [P; Z] ∧ (∀P′Z′.T [P′; Z′] ⊃ ¬(P′ < P)),

where P and Z are disjoint lists of predicate constants and T [P′; Z′] is T with each predicate symbol p in P Z replaced by p′. All remaining predicates not in P Z (the Q predicates) are fixed. Note that unlike in [10, 11], functions are not allowed to vary. For convenience, we denote the circumscription of T under minimization of all predicates (Q = Z = ∅) by CIRC (T ).

de Kleer and Konolige have shown how to eliminate fixed predicates from a circumscription efficiently (even in linear time) [2]; thus we may assume that no fixed predicates occur in T . Further, we may assume without loss of generality that in any instance of CIRC (T ; P; Z) ⊧ F all predicates in the formula F occur in T : if a predicate p does not occur in T , simply join a tautology involving only p (e.g., (∀x.p(x) ⊃ p(x)) ) to T .

The transformation is as follows:

Definition 2.1 (reduction) Let T , F be first-order formulas, and let the lists P, Z partition the predicate symbols in T . The first-order formula Γ(T ; F; P; Z) is defined as follows:

Γ(T ; F; P; Z) = (P Z ≡ ¬P′′Z′′) ∧ [(u ∧ (P′Z′ ≡ true)) ∨ (¬u ∧ Θ(P, Z, P′, Z′))]

where Θ(P, Z, P′, Z′) is the formula (T ⊃ F) ∨ (T [P′; Z′] ∧ (P′ < P)).

Let us first give a rough intuitive explanation of this transformation. The predicates P′′ and Z′′ and the formula P Z ≡ ¬P′′Z′′ are added in order to make structures with different extensions of P Z incomparable. Hence, minimization has no effect on the predicates from P ZP′′Z′′. This allows us to “simulate” standard semantics within a circumscription where all predicates are minimized. The only predicates in CIRC (Γ(T ; F; P; Z)) that are effectively minimized are those in P′Z′ and u. Therefore, CIRC (Γ(T ; F; P; Z)) ⊧ ¬u holds iff in each P; Z-minimal model of Γ(T ; F; P; Z), the formula Θ(P, Z, P′, Z′) is satisfied. This means that for each extension of P and Z, either T ⊃ F, or the extension is not P; Z-minimal; in other words, CIRC (T ; P; Z) ⊧ F holds.

For examples of this transformation, refer to the appendix, where its application is demonstrated for two well-known examples for inferencing under circumscription.

In the sequel, we formally prove that CIRC (T ; P; Z) ⊧ F iff CIRC (Γ(T ; F; P; Z)) ⊧ ¬u. To this end, we first show a lemma stating that testing the validity of formulas belonging to a certain fragment of second order logic can be reduced to an inference problem under circumscription where all predicates are minimized. In order to show our main result, we then make use of this transformation.

Definition 2.2 Let Ψ be a second-order formula of the form ∀A∃B Φ(A, B) where A, B are disjoint lists of predicate variables and Φ(A, B) is a first-order formula. Denote by τ(Ψ) the following first-order formula:

(A ≡ ¬A′′) ∧ [(u ∧ (B ≡ true)) ∨ (¬u ∧ Φ(A, B))].

Lemma 2.1 Let Ψ be a second-order formula of the form ∀A∃B Φ(A, B) where A, B are disjoint lists of predicate variables and Φ(A, B) is a first-order formula containing no other predicate symbols except those in A and B. Then, Ψ is valid if and only if CIRC (τ(Ψ)) ⊧ ¬u.

Proof:

We first observe that for any possible universe U, τ(Ψ) has for any interpretation of the function symbols and any extension E of the A-predicates over U, a unique model M such that |M| = U, [[ A]]_{M} = E, M ⊧ u, and M ⊧ (∀x.b(x)) for every b from B. Furthermore, if any two models M, M′ of τ(Ψ) satisfy [[ A]]_{M} ≠ [[ A]]_{M′}, then neither M < M′ nor M′ < M.

Now assume that Ψ is valid but CIRC (τ(Ψ)) ⊧ ¬u is false. This means that there is a minimal model M of τ(Ψ) such that u is true in M. Observe that [[ B]]_{M} is the maximum possible extension of B over |M| because M satisfies (B ≡ true). Since Ψ is valid, for the same extension of all function symbols, there must exist an extension E of B over |M| such that Φ( [[ A]]_{M}, E) is true over |M|. Now consider the structure M′ with the same interpretation of functions as M and [[ AA′′]]_{M′} = [[ AA′′]]_{M}, [[ B]]_{M′} = E, and u is false. Since M′ ⊧ ¬u, and M′ ⊧ Φ( [[ A]]_{M}, E), it is a model of τ(Ψ). As [[ AA′′]]_{M′} = [[ AA′′]]_{M}, [[ B]]_{M′} ≤ [[ B]]_{M} and [[ u]]_{M′} < [[ u]]_{M}, we have M′ < M. This is a contradiction to the minimality of M, however.

Conversely, assume that CIRC (τ(Ψ)) ⊧ ¬u holds. Let E be an arbitrary extension of the A-predicates over some universe U. By our observation from above, there exists for any U and any function interpretation over U a model M of τ(Ψ) such that |M| = U, [[ A]]_{M} = E, and M ⊧ u. From CIRC (τ(Ψ)) ⊧ ¬u it follows that M cannot be minimal; hence there exists a model M′ < M with [[ A]]_{M′} = [[ A]]_{M} where u is not satisfied. (Clearly u cannot be satisfied in any model M′ < M: Any such M′ must satisfy |M′| = |M| = U and [[ A]]_{M′} = [[ A]]_{M}, and since M is for this function interpretation the unique model of τ(Ψ) over U satisfying [[ A]]_{M} = E and M ⊧ u, M′ ⊧ ¬u must hold; hence, M′ must satisfy ¬u ∧ Φ(A, B), the second term of the disjunction in τ(Ψ).) Consequently, Φ( [[ A]]_{M′}, [[ B]]_{M′}) is true over U under that function interpretation. Since U, the function interpretation and the extension E = [[ A]]_{M′} of the A-predicates over U were arbitrary, it follows that ∀A∃B Φ(A, B) is true over any universe U under any function interpretation, and hence Ψ is valid. □

Theorem 2.2 Let T , F be first-order formulas such that all predicates in F appear in T , and let the lists P, Z partition the predicates in T . Then, CIRC (T ; P; Z) ⊧ F if and only if CIRC (Γ(T ; F; P; Z)) ⊧ ¬u.

Proof:

CIRC (T ; P; Z) ⊧ F holds iff F is valid in every P; Z-minimal model of T [10, Proposition 1], that is CIRC (T ; P; Z) ⊧ F is true iff every model of T is also a model of F or not a P; Z-minimal model of T . Thus CIRC (T ; P; Z) ⊧ F is true iff the second-order formula (∀P Z.(T [P; Z] ⊃ F) ∨ (∃P′Z′.(T [P′; Z′] ∧ (P′ < P)))) is valid, which is equivalent to the following formula Ψ[T ; F; P; Z]:

(∀P Z ∃P′Z′.(T [P; Z] ⊃ F) ∨ (T [P′; Z′] ∧ (P′ < P))).

Note that Ψ[T ; F; P; Z] is of the form ∀A∃B Φ(A, B), where Φ(A, B) is a first-order formula and A = P Z, B = P′Z′. Note that ∀A∃BΦ(A, B) satisfies the conditions on the formula Ψ in Lemma 2.1. Since τ(∀A∃B Φ(A, B)) is the first-order formula (A ≡ ¬A′′) ∧ [(u ∧ (B ≡ true)) ∨ (¬u ∧ Φ(A, B))], we thus get by Lemma 2.1 that CIRC (T ; F; Z) ⊧ F iff ¬u follows from the circumscription of the first-order formula

(P Z ≡ ¬P′′Z′′) ∧ [(u ∧ (P′Z′ ≡ true)) ∨ (¬u ∧ ((T ⊃ F) ∨ (T [P′; Z′] ∧ (P′ < P))))].

The latter formula is just the formula Γ(T ; F; P; Z); thus CIRC (T ; P; Z) ⊧ F iff CIRC (Γ(T ; F; P; Z)) ⊧ ¬u. □

Remark. Lemma 2.1 and Theorem 2.2 put together are a simple proof for the fact that the problem of inferencing under circumscription, whether or not varying predicates are used, is precisely equivalent to the problem of checking the validity of a second-order formula belonging to the Π_{2}^{1}-level of the prenex hierarchy of second-order logic. By a well-known result of Hintikka [8], this problem (as well as validity checking for any higher-order formula) can be effectively reduced to validity checking of a monadic Σ_{1}^{1} second-order formula as long as standard models are considered (see also [18]). Thus, under standard model semantics in the sense of [18], the inference problem under circumscription, with varying predicates as well as without, is complete for the class Σ_{1}^{1}. This complements a result of Schlipf [17], who has shown that the same problem restricted to countably infinite models is Π_{2}^{1}(N)-complete, that is Π_{2}^{1}-complete over the natural numbers. (Note that the class Π_{2}^{1}(N) of the analytic hierarchy is strictly more expressive than the class Σ_{1}^{1}(N).)

The transformation as a syntactic reduction is feasible in linear time and hence very efficient. The question of how it affects the complexity of the derivation is rather intricate, however. On the one hand, our transformation adds new predicate symbols to the initial formula that lead to additional computational overhead. Also, some methods require the input to be in a special form. As an example, Przymusinski’s method requires the circumscribed formula to be in clausal form. Hence, in order to use our transformation, the first step is to compute the clausal form of Γ(T ; F; P; Z). This computation may be very expensive, sometimes more expensive than transforming T itself into clause form. On the other hand, our transformation eliminates the handling of varying predicates, which constitutes a substantial part of most derivation algorithms. In Przymusinski’s algorithm for instance, this step may cause exponential overhead. In summary, our transformation shifts the burden of handling varying predicates to predicate minimization.

An application of our transformation to closed-world reasoning is also possible. This technique for non-monotonic reasoning is closely related to circumscription [3, 10, 5] and has been defined in several ways. In its previous versions (CWA, GCWA, EGCWA [16, 14, 19]), the closed-world assumption was applied to all the predicates. In its more recent definitions (CCWA, ECWA [6, 5]) it is possible to vary a predicate, and the intended meaning of this variability is the same as in circumscription. Notice that the Extended Closed World Assumption (ECWA), which like circumscription minimizes some predicates P while varying other predicates Z and fixing the remaining predicates Q, is the most general rule for closed-world reasoning, extending all other versions of closed world-reasoning mentioned above.

Lifschitz demonstrated in [10] that for function-free first-order theories, the CWA under the assumptions of domain-closure and unique names is equivalent to predicate circumscription where all predicates are minimized, provided CWA is consistent. Gelfond et al. show in [5] that under the same assumptions the closure of a theory under ECWA for P, Z is equivalent to predicate circumscription under identical P, Z. Thus our method can fruitfully be applied for simplifying closed-world reasoning. In particular, it is possible to reduce inferencing under ECWA to inferencing under the Extended Generalized Closed World Assumption (EGCWA) defined in [19], since this rule is identical to ECWA for Q = Z = ∅ [5].

3 Conclusions

We have introduced an efficient method to reduce inference under predicate circumscription to inferencing under circumscription where all predicates are minimized, and we proved its correctness. This reduction can be performed in linear time. We believe that the method provides new insights into the relation between the general form of predicate circumscription and circumscription without varying predicates. The same applies to different versions of closed-world reasoning. Furthermore, the method can be practically used to build theorem provers for predicate circumscription out of existing simpler inference engines or procedures for circumscription without varying predicates (e.g., the algorithm by Bossu and Siegel [1]). The new method even allows noticeable simplifications to familiar algorithms to answer queries under predicate circumscription. For instance, Przymusinski’s well-known query answering algorithm based on MILO-resolution [15] involves a separate treatment for variable predicates that can be bypassed by our transformation.

A Appendix

To illustrate the transformation, we consider the classic examples of Tweety the bird and Sam the penguin.

Example 1 Let our knowledge base be the following:

T = b(T weety) ∧ (∀x.b(x) ∧ ¬ab(x) ⊃ f(x)).

(The intended meaning of b is “is a bird”, of ab is “is abnormal”, and of f is “flies”). The list P of the predicates to be minimized contains only ab, while the remaining predicates b and f are the varying predicates Z. It is well-known that CIRC (T ; P; Z) ⊧ f(T weety) (see, for example [6, 9]). The transformation we defined previously yields the following formula:

Γ(T ; f(T weety); P; Z) = [(ab, b, f) ≡ ¬(ab′′, b′′, f′′)] ∧
[(u ∧ (ab′, b′, f′ ≡ true)) ∨ (¬u ∧ Θ(ab, b, f, ab′, b′, f′))],

where Θ(ab, b, f, ab′, b′, f′) = [(T ⊃ f(T weety)) ∨ (T [ab′; b′, f′] ∧ (ab′ < ab))]. Substituting for our notation, we get

Γ(T ; f(T weety); P; Z) = C_{1} ∧ C_{2} ∧ C_{3} ∧ [(u ∧ D_{1}) ∨ (¬u ∧ (D_{2} ∨ D_{3}))],

where

C_{1} = (∀x.b(x) ≡ ¬b′′(x)),

C_{2} = (∀x.f(x) ≡ ¬f′′(x)),
C_{3} = (∀x.ab(x) ≡ ¬ab′′(x)),
D_{1} = (∀x.b′(x)) ∧ (∀x.f′(x)) ∧ (∀x.ab′(x)),
D_{2} = [b(T weety) ∧ (∀x.b(x) ∧ ¬ab(x) ⊃ f(x))] ⊃ f(T weety),
D_{3} = [b′(T weety) ∧ (∀x.b′(x) ∧ ¬ab′(x) ⊃ f′(x)) ∧
(∀x.ab′(x) ⊃ ab(x)) ∧ (∃x.¬ab′(x) ∧ ab(x))].

We show that CIRC (Γ(T ; f(T weety); P; Z)) ⊧ ¬u: Suppose that there exists a minimal model M of Γ(T ; f(T weety); P; Z) such that M ⊧ u; clearly M |̸= D_{2} ∨ D_{3}, otherwise the interpretation N of T which is equivalent to M everywhere but not in u (N |̸= u) would be a model of Γ(T ; f(T weety); P; Z) such that N < M, but this contradicts the hypothesis that M is a minimal model of Γ(T ; f(T weety); P; Z). Notice that M |̸= D_{2} implies M ⊧ ab(T weety). Moreover M ⊧ D_{1}, since M is a model of Γ(T ; f(T weety); P; Z). We can define a new interpretation L of Γ(T ; f(T weety); P; Z) such that L is equivalent to M everywhere but not in u or in ab′ such that L ⊧ ¬u ∧ ∀x.¬ab′(x). Since M ⊧ D_{1}, it follows that L ⊧ (∀x.b′(x)) ∧ (∀x.f′(x)). Since M ⊧ ab(T weety), it follows that L ⊧ ab(T weety). It follows from this L ⊧ D_{3}; this means that L is a model of Γ(T ; f(T weety); P; Z). But L < M, which contradicts the hypothesis that M is minimal.

Playing devil’s advocate, let us see if we can prove more from CIRC (Γ(T ; F; P; Z)) than what is available from CIRC (T ; P; Z). Suppose we add walk(George) to T (let T′ = T ∧walk(George) ) and try to prove walk(T weety) from CIRC (Γ(T′; walk(T weety); P; Z)), where P = ab and Z = b, f, walk. Assuming T weety ≠ George, choose the following extensions for ab, b, f, walk: ∀x.ab(x) ≡ false, ∀x.b(x) ≡ x = T weety, ∀x.f(x) ≡ x = T weety, and ∀x.walk(x) ≡ x = George. This induces a minimal model of T′ in which walk(T weety) is false. Therefore, Θ(ab, b, f, walk, ab′, f′, walk′) in the reduction of T′ is false in that case; hence, if u is true, if ab′, b′, f′, walk′ ≡ true holds, and if we select the double primed predicates appropriately, we obtain a minimal model of Γ(T′; walk(T weety); P; Z) in which u is true. Therefore, CIRC (Γ(T′; walk(T weety); P; Z)) |̸= ¬u. □

Example 2 We will consider the classic example of Sam the penguin. Our knowledge base is the following:

T = p(Sam) ∧ (∀x.p(x) ⊃ b(x)) ∧
(∀x.b(x) ∧ ¬ab_{1}(x) ⊃ f(x)) ∧
(∀x.p(x) ∧ ¬ab_{2}(x) ⊃ ¬f(x))

(Here p is intended to mean “is a penguin”, ab_{1} and ab_{2} grasp different kinds of abnormality, and b, f are as above). P contains ab_{1}, ab_{2}, while Z is p, b, f. CIRC (T ; P; Z) ⊧ f(Sam) does not hold (indeed, the extensions ∀x.ab_{1}(x) ≡ x = Sam, ∀x.ab_{2}(x) ≡ false, ∀x.p(x) ≡ x = Sam, ∀x.b(x) ≡ x = Sam, ∀x.f(x) ≡ false induce a P; Z-minimal model of T in which f(Sam) is not satisfied). Our transformation yields the following formula:

Γ(T ; f(Sam); P; Z) = [(ab_{1}, ab_{2}, p, b, f) ≡ ¬(ab′′_{1}, ab′′_{2}, p′′, b′′, f′′)] ∧
[(u ∧ (ab′_{1}, ab′_{2}, p′, b′, f′ ≡ true)) ∨ (¬u ∧ Θ(P, Z, P′, Z′))],

where

Θ(P, Z, P′, Z′) = [(T ⊃ f(Sam)) ∨ (T [ab′_{1}, ab′_{2}; p′, b′, f′] ∧ (ab′_{1}, ab′_{2} < ab_{1}, ab_{2}))].

That is,

Γ(T ; f(Sam); P; Z) = C_{1} ∧ C_{2} ∧ C_{3} ∧ C_{4} ∧ C_{5} ∧ [(u ∧ D_{1}) ∨ (¬u ∧ (D_{2} ∨ D_{3}))],

where

C_{1} = (∀x.p(x) ≡ ¬p′′(x)),
C_{2} = (∀x.b(x) ≡ ¬b′′(x)),
C_{3} = (∀x.f(x) ≡ ¬f′′(x)),
C_{4} = (∀x.ab_{1}(x) ≡ ¬ab′′_{1}(x)),
C_{5} = (∀x.ab_{2}(x) ≡ ¬ab′′_{2}(x)),
D_{1} = (∀x.p′(x)) ∧ (∀x.b′(x)) ∧ (∀x.f′(x)) ∧ (∀x.ab′_{1}(x)) ∧ (∀x.ab′_{2}(x)),
D_{2} = [p(Sam) ∧ (∀x.p(x) ⊃ b(x)) ∧ (∀x.b(x) ∧ ¬ab_{1}(x) ⊃ f(x)) ∧
(∀x.p(x) ∧ ¬ab_{2}(x) ⊃ ¬f(x))] ⊃ f(Sam)
D_{3} = p′(Sam) ∧ (∀x.p′(x) ⊃ b′(x)) ∧ (∀x.b′(x) ∧ ¬ab′_{1}(x) ⊃ f′(x)) ∧
(∀x.p′(x) ∧ ¬ab′_{2}(x) ⊃ ¬f′(x)) ∧
(∀x.ab′_{1}(x) ⊃ ab_{1}(x)) ∧ (∀x.ab′_{2}(x) ⊃ ab_{2}(x)) ∧
[(∃x.¬ab′_{1}(x) ∧ ab_{1}(x)) ∨ (∃x.¬ab′_{2}(x) ∧ ab_{2}(x))].

We show that CIRC (Γ(T ; f(Sam); P; Z)) |̸= ¬u by identifying a minimal model M of Γ(T ; f(Sam); P; Z) such that M ⊧ u. M is characterized as follows :

M ⊧ u ∧ (∀x.p′(x) ∧ b′(x) ∧ f′(x) ∧ ab′_{1}(x) ∧ ab′_{2}(x))

that is, M satisfies D_{1},

M ⊧ p(Sam) ∧ b(Sam) ∧ ¬f(Sam) ∧ ab_{1}(Sam) ∧ ¬ab_{2}(Sam) ∧
¬p′′(Sam) ∧ ¬b′′(Sam) ∧ f′′(Sam) ∧ ¬ab′′_{1}(Sam) ∧ ab′′_{2}(Sam)

and

\begin{aligned}M & ⊧ & (∀x.x ≠ Sam ⊃ & [¬p(x) ∧ ¬b(x) ∧ ¬f(x) ∧ ¬ab_{1}(x) ∧ ¬ab_{2}(x)∧ \\ & & & p′′(x) ∧ b′′(x) ∧ f′′(x) ∧ ab′′_{1}(x) ∧ ab′′_{2}(x)]), \end{aligned}

that is, every predicate from the original theory T is false in M for every constant different from Sam. Note that M is a model of Γ(T ; F; P; Z), because M ⊧ C_{1} ∧ C_{2} ∧ C_{3} ∧ C_{4} ∧ C_{5} ∧ u ∧ D_{1}. Minimality of M can be seen as follows. Assume that M is not minimal, that is there is a model N of Γ(T ; f(Sam); P; Z) such that N < M. N can only decrease the predicates ab′_{1}, ab′_{2}, p′, b′, f′, because decreasing any other predicate forces another predicate to increase. This implies that N |̸= D_{1}, therefore N ⊧ D_{2}∨D_{3} must be true; but M ⊧ ¬D_{2}, and since the predicates in D_{2} have the same extension in M and N, N ⊧ ¬D_{2} holds; hence, N ⊧ D_{3} must hold. Since ab_{1}(Sam) is the only ground atom of ab_{1}(x), ab_{2}(x) that is true in M and hence also in N, we infer from the last conjunct of D_{3} that N ⊧ ¬ab′_{1}(Sam). Since D_{3} ⊧ b′(Sam)∧(∀x.b′(x)∧¬ab′_{1}(x) ⊃ f′(x)), it follows that N ⊧ f′(Sam). Since D_{3} ⊧ p′(Sam) ∧ (∀x.p′(x) ∧ ¬ab′_{2}(x) ⊃ ¬f′(x)), it follows that M ⊧ ab′_{2}(Sam). But D_{3} ⊧ (∀x.ab′_{2}(x) ⊃ ab_{2}(x)); thus it follows that N ⊧ ab_{2}(Sam). This leads to a contradiction, however, since M ⊧ ¬ab_{2}(Sam) and hence N ⊧ ¬ab_{2}(Sam) must hold. Therefore N cannot exist, and M is truly a minimal model of Γ(T ; f(Sam); P; Z). Thus CIRC (Γ(T ; f(Sam); P; Z)) |̸= ¬u is proved.

We close the example considering a small change to our knowledge base T . Suppose the bird Tweety from Example 1 appears in Sam′s world, and let T′ = T ∧ b(T weety). Under the unique-names assumption (T weety ≠ Sam), can we still prove that Tweety flies under minimization of abnormality while the other predicates vary ? Indeed, under this assumption CIRC (T′; P; Z) ⊧ f(T weety) holds. This can be seen as follows. There exist models of T′ in which ab_{1}(T weety) and ab_{2}(T weety) are false, and in each of them p(T weety) is false. Thus for inferencing f(T weety) under circumscription, T′ essentially reduces to the knowledge base T in Example 1 where ab and ab_{1} need to be collapsed. Therefore, one can show that CIRC (Γ(T′; f(T weety); P; Z)) ⊧ ¬u holds along a line of argumentation similar to that in Example 1. □

Acknowledgment

The authors would like to thank the anonymous referees for their helpful comments and suggestions to improve a previous draft of this paper. They are also grateful to Alex Leitsch for hints on references.

References

[1] G. Bossu and P. Siegel. Saturation, Nonmonotonic Reasoning and the Closed

World Assumption. Artificial Intelligence, 25:13–63, 1985.

[2] J. de Kleer and K. Konolige. Eliminating the Fixed Predicates from a Circumscription. Artificial Intelligence, 39:391–398, 1989.

[3] D. W. Etherington, R. E. Mercer, and R. Reiter. On the Adequacy of Predicate Circumscription for Closed World Reasoning. Computational Intelligence, 1:11– 15, 1985.

[4] D. W. Etherington. Reasoning with Incomplete Information. Morgan Kaufmann Publishers, Inc., Los Altos, 1988.

[5] M. Gelfond, H. Przymusinksa, and T. Przymusinski. On the Relationship Between Circumscription and Negation as Failure. Artificial Intelligence, 38:75–94, 1989.

[6] M. Gelfond and H. Przymusinska. Negation as Failure: Careful Closure Procedure. Artificial Intelligence, 30:273–287, 1986.

[7] M. L. Ginsberg. A Circumscriptive Theorem Prover. Artificial Intelligence, 39:209–230, 1989.

[8] J. Hintikka. Reductions in the Theory of Types. Acta Philosophica Fennica, 8:61–115, 1955.

[9] V. Lifschitz. Closed-World Databases and Circumscription. Artificial Intelligence, 27:229–235, 1985.

[10] V. Lifschitz. Computing Circumscription. In Proceedings IJCAI-85, pages 121– 127, 1985.

[11] V. Lifschitz. Pointwise Circumscription. In Proceedings AAAI-86, pages 406–410, 1986.

[12] J. McCarthy. Circumscription – A Form of Non-Monotonic Reasoning. Artificial Intelligence, 13:27–39, 1980.

[13] J. McCarthy. Applications of Circumscription to Formalizing Common-Sense Knowledge. Artificial Intelligence, 28:89–116, 1986.

[14] J. Minker. On Indefinite Data Bases and the Closed World Assumption. In Proceedings of the 6^{th} Conference on Automated Deduction (CADE), pages 292– 308, 1982.

[15] T. Przymusinski. An Algorithm to Compute Circumscription. Artificial Intelligence, 38:49–73, 1989.

[16] R. Reiter. On Closed-World Databases. In H. Gallaire and J. Minker, editors, Logic and Data Bases, pages 55–76. Plenum Press, New York, 1978.

[17] J.S. Schlipf. Decidability and Definability with Circumscription. Annals of Pure and Applied Logic, 35:173–191, 1987.

[18] J. van Benthem and K. Doets. Higher Order Logic. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, Vol.I, chapter I.4, pages 275–329. D. Reidel Publishing Company, 1983.

[19] A. Yahya and L. Henschen. Deduction in Non-Horn Databases. Journal of Automated Reasoning, 1(2):141–160, 1985.

[20] L.Y. Yuan and C.H. Wang. On Reducing Parallel Circumscription. In Proceedings AAAI-88, pages 460–464, 1988.