Circumscription

Tom Costello

April 9, 1998

0.1 Domain Circumscription

McCarthy’s original example of non-monotonic reasoning was about the lack of a bridge (in the missionaries and cannibals problem)[Ama68]. The idea of minimizing objects was therefore the first attempted solution. All of the objects in the problem were minimized—if they could fail to exist, then they were assumed not to exist.

Historically, domain circumscription was the earliest form of circumscription. It was introduced in [McC77]. It was studied by Davis[Dav80], and further investigated by Etherington and Mercer[EM87].

Domain description tries to capture the intuition that as few objects exist as possible. It attempts to carry out something like domain closure[Rei87], that is to state that the only objects that exist are those that must exist.

The model theory for domain circumscription is applicable to arbitrary classes of models, however the syntactic form of domain circumscription restricts the set of theories to those axiomatizable by a finite set of first order sentences.

We now look at McCarthy’s definition of domain circumscription. We need an auxiliary definition of a formula which McCarthy called^{1} Axiom(ϕ), but which we call Closed_{L}(ϕ), as it states that ϕ is closed under the application of all the functions in L.

Definition: 1 (Closed_{L}(ϕ)) If ϕ is a unary predicate variable, Closed_{L}(ϕ) stands for the conjunction of ϕ(c) for every constant c in the language L, and the ∀x_{1} …, x_{n}.ϕ(x_{1}) ∧ … ϕ(x_{n}) → ϕ(f(x_{1}, …, x_{n})), for each n-ary function constant f in L.

We also need the standard notion of the relativization of a formula by a unary predicate.

Definition: 2 The relativization of a formula γ with respect to a unary predicate variable ϕ, written γ^{ϕ}, is the result of replacing ∀x. and ∃x. by ∀x.ϕ(x) → and ∃x.ϕ(x)∧ in γ, defined inductively as follows.

1We use ϕ for unary predicate variables, ψ for predicate variables of arbitrary arity, β, γ, δ for formulas, α for sentences, L for languages, ζ for function variables, x, y, z, v, l, p for individual variables, t for terms, Γ, Δ, for sets of formulas, \overline{P} , Z for sets of predicates, capital Roman letters or words for predicate symbols, f for function symbols, c and capital Roman letters for constant symbols, a, b for objects, German font for models, U for domains, S for sorts, and K to range over all constants in a language. All of these may have subscripts. We note that α′ is used as a abbreviation, not as a formula name.

• If γ = P (t_{1}, …, t_{n}) then γ^{ϕ} = P (t_{1}, …, t_{n}).

• If γ = α ∧ β then γ^{ϕ} = α^{ϕ} ∧ β^{ϕ}.

• If γ = α ∨ β then γ^{ϕ} = α^{ϕ} ∨ β^{ϕ}.

• If γ = α → β then γ^{ϕ} = α^{ϕ} → β^{ϕ}.

• If γ = ¬α then γ^{ϕ} = ¬α^{ϕ}.

• If γ = α ≡ β then γ^{ϕ} = α^{ϕ} ≡ β^{ϕ}.

• If γ = ∃x.α then γ^{ϕ} = ∃x.ϕ(x) ∧ α^{ϕ}.

• If γ = ∀x.α then γ^{ϕ} = ∀x.ϕ(x) → α^{ϕ}. If ϕ_{1}, ϕ_{2} is a sequence of predicate variables, then γ^{ϕ_{1},ϕ_{2}} denotes the iterated relativization of γ, i.e. (γ^{ϕ_{1}})^{ϕ_{2}}.

Definition: 3 The domain circumscription of the sentence α in a language L, denoted DomCirc_{L}(α), is the following formula of second order logic.

α ∧ ∀ϕ.Closed_{L}(ϕ) ∧ α^{ϕ} → ∀x.ϕ(x)

where ϕ is a one place predicate variable.

Domain circumscription has a natural semantics. We say that one model 𝔄 is ≤_{domain} than another model 𝔅, if and only if 𝔄 is a sub-model of 𝔅. By this we mean that 𝔄 is the reduct of 𝔅 to the domain of 𝔄. The relation sub-model naturally forms a pre-order. The minimal models under this pre-order are the intended models of domain circumscription.

Definition: 4 For a given language L and two L-structures, 𝔄 and 𝔅, we say that 𝔄 ≤_{domain} 𝔅, if and only if 𝔄 is a sub-model of 𝔅.

Example: 1 Let the sentence α be the conjunction of the following sentences:

Bird(T weety) ∧ P enguin(Opus),  (1)
∀x.P enguin(x) → Bird(x).  (2)

The domain circumscription of this theory is the above sentences conjoined with, ∀ϕ.[ϕ(T weety) ∧ ϕ(Opus) ∧ Bird(T weety) ∧ P enguin(Opus)∧

∀x.[ϕ(x) → (P enguin(x) → Bird(x))]] → ∀x.ϕ(x).

This entails,

∀x.x = T weety ∨ x = Opus.

In fact it is equivalent to,

(∀x.x = T weety ∨ x = Opus) ∧ Bird(T weety) ∧ Bird(Opus) ∧ P enguin(Opus),

that is, it has three models, one containing a single object which is both a penguin and a bird, and two models containing two objects, one called Tweety, one called Opus, where all objects are birds, and either just Opus is a penguin, or both birds are Penguins.

To show this we use the standard trick[Lif85] of removing second order quantifiers. We do this by instantiating the quantifier ∀ϕ by λx.x = T weety ∨ x = Opus.

1 Theorem: (McCarthy 1977,Soundness) Let ⊢ represent any sound proof theory for second order logic.

If DomCirc_{L}(α) ⊢ γ then γ is true in every minimal model of α under the pre-order ≤_{domain}.

Etherington and Mercer modified the definition of domain circumscription by adding a conjunct, ∃x.ϕ(x), to the left hand side of the implication in the definition. This is only of interest in the case when the signature of the language contains no constants. If the language contains a constant c, ϕ(c) is added as part of Closed_{L}. As ϕ(c) implies ∃x.ϕ(x), adding ∃x.ϕ(x) makes no difference in this case. From now on we assume that there are some constants.

0.2 Predicate Circumscription

McCarthy introduced a new form of circumscription predicate circumscription[McC80]. This form of circumscription differed greatly from domain circumscription. It was not an extension, there being problems that domain circumscription could solve that predicate circumscription could not.

It was also based on minimization, but rather than minimize the amount of objects in the domain, it minimized the extension of a predicate symbol. McCarthy originally defined it as a first order logic schema, however it is more easily understood as a sentence of second order logic.

Definition: 5 (≤, < on formulas) It is useful to introduce the notation γ_{1}, γ_{2} ≤ δ_{1}, δ_{2} for the formula (∀\overline{x}.γ_{1}(\overline{x}) → δ_{1}(\overline{x})) ∧ (∀\overline{y}.γ_{2}(\overline{y}) → δ_{2}(\overline{y})), and γ_{1}, γ_{2} < δ1, δ_{2} for the formula γ_{1}, γ_{2} ≤ δ_{1}, δ_{2} ∧ ¬(δ_{1}, δ_{2} ≤ γ_{1}, γ_{2}), where \overline{x} and \overline{y} are sequences of variables equal in number to the free variables of γ_{1}, δ_{1} and γ_{2}, δ_{2}.

This definition of predicate circumscription does not allow “varied” predicates. We later look at formula circumscription, a version that does allow varied predicates. McCarthy[McC80] suggested varying predicates, but gave no examples. In our definitions of circumscription from now on we assume that we minimize two formulas/predicates, in a language with one or two predicate symbols, one function symbol, and one constant. The extension to n predicates/formulas, and larger languages is the obvious one.

Definition: 6 Let L be a first order language with equality, whose predicates include P_{1}, P_{2}. Let α be a sentence in L. The circumscription of α minimizing P_{1}, P_{2}, denoted Circ_{P} (α; P_{1}, P_{2}) is the second order formula:

α ∧ ∀ψ_{1}, ψ_{2}.¬ [α[ψ_{1}/P_{1}, ψ_{2}/P_{2}] ∧ ψ_{1}(\overline{x}), ψ_{2}(\overline{y}) < P_{1}(\overline{x}), P_{2}(\overline{y})]

where ψ_{1} and ψ_{2} are predicate variables equal in arity to P_{1} and P_{2}, and \overline{x}, \overline{y} are tuples of variables.

We now introduce semantics for predicate circumscription. We use A to denote the domain of 𝔄, and 𝔄[K] to denote the interpretation of K in 𝔄.

Definition: 7 Let α be a sentence of L, a first order language with equality, whose predicates are {P_{1}, …, P_{n}}. Let \overline{P} be a subset of P_{1}, …, P_{n}. A model 𝔄 of α is a \overline{P} -sub-model of a model 𝔅, written 𝔄 ≤\overline{P} 𝔅, if and only if:

• A = B, that is the domains of 𝔄 and 𝔅 are equal.

• 𝔄[K] ⊆ 𝔅[K], for every predicate constant K ∈ \overline{P},

• 𝔄[K] = 𝔅[K], for every function, object, or predicate constant K not in \overline{P}.

𝔄 is \overline{P} -minimal model of A if and only if no other model of α is a \overline{P} -sub-model of 𝔄.

2 Theorem: (McCarthy 80) Let α, γ be sentences of L, a first order language with equality, whose predicates are {P_{1}, …, P_{n}}. Let \overline{P} be a subset of P_{1}, …, P_{n}.

If ⊢ is a sound inference system for second order logic, then if Circ_{P} (α; \overline{P}) ⊢ γ then γ is true in every \overline{P} -minimal model of α.

We now look at a simple example of circumscription, taken from Lifschitz[Lif85].

Example: 2 Consider the language L, with a unary predicate P and three constants B, C, and D, let the sentence α be P (D) ∨ (P (B) ∧ P (C)), then

Circ_{P} (α; P) ≡ (∀x.P (x) ≡ x = D) ∨ (∀x.P (x) ≡ x = B ∨ x = C ∧ D ≠ B ∧ D ≠ C).

0.3 Formula Circumscription

McCarthy[McC86] introduced a new form of circumscription, called formula circumscription. It extends predicate circumscription in two ways.

• The new form of circumscription allows the extensions of arbitrary formulas to be minimized rather than only minimizing predicates.

• Certain predicates are allowed to be varied in the minimization process. This notion was suggested, but not explored, by McCarthy[McC80].

Definition: 8 If γ_{1}, γ_{2} is a pair of formulas of a first order language L, and P_{1} is a predicate symbol of L, then the circumscription of α minimizing γ_{1}, γ_{2}, formulas in L, varying P_{1}, written Circ_{F} (α; γ_{1}, γ_{2}; P_{1}) is,

α ∧ ∀ψ_{1}.¬ [α′ ∧ γ′_{1}, γ′_{2} < γ_{1}, γ_{2}]

where ψ_{1} is a predicate variable equal in arity to P_{1}. We use α′ to denote the formula, α[ψ_{1}/P_{1}], that is the replacement of the predicate P_{1} in α by a predicate variable.

We now introduce the semantics for formula circumscription.

Definition: 9 Let α be a sentence of L, a first order language with equality, whose predicates are P_{1}, …, P_{n}. Let Z be a subset of P_{1}, …, P_{n}. A model 𝔄 of α is a γ_{1}, … γ_{n}; Z-sub-model of a model 𝔅, written 𝔄 ≤_{γ_{1},...γ_{n};Z} 𝔅, if and only if:

• ∥𝔄∥ = ∥𝔅∥,

• 𝔄[γ_{i}] ⊆ 𝔅[γ_{i}], for i = 1 … n.

• 𝔄[K] = 𝔅[K], for every function, object, or predicate constant not in Z.

𝔄 is a γ_{1}, … γ_{n}; Z-minimal model of A if and only if it is a minimal model of α under ≤_{γ_{1},...γ_{n};Z}.

3 Theorem: (McCarthy 1986) Let α, β, γ_{1}, …, γ_{n} be sentences of L, a first order language with equality, whose predicates are {P_{1}, …, P_{n}}. Let Z be a subset of P_{1}, …, P_{n}.

If ⊢ is a sound inference system for second order logic, then If Circ_{F} (α; γ_{1}, …, γ_{n}; Z) ⊢ β then β is true in every γ_{1}, … γ_{n}; Z-minimal model of α.

0.4 Second Order Circumscription

Lifschitz[Lif85] modifies the definition of circumscription to allow the varied symbols to include constant or function symbols.

deKleer and Konolige prove[dKK89] that not varying a predicate symbol, in formula circumscription, can be expressed by minimizing both the predicate symbol and its negation. Thus we may assume that all predicates are varied.

Definition: 10 (Circ(α; Γ)) If γ_{1}, γ_{2} is a pair of formulas in a first order language L, and P, f, c are the predicates, functions and constants in L, then we define the circumscription of a sentence α in L minimizing γ_{1}, γ_{2}, written Circ(α; γ_{1}, γ_{2}) as follows. We use α′ to denote the formula α[ψ/P, ζ/f, x/c], that is the replacement of the predicates P, functions F and constants c in α by predicate, function and constant variables, ψ, ζ and x, respectively.

α ∧ ∀ψ, ζ, x.¬ [α′ ∧ γ′_{1}, γ′_{2} < γ_{1}, γ_{2}] ,

where ψ and ζ are predicate, function variables respectively agreeing in arity with P and f, and x is an individual variable.

Definition: 11 (≤_{Γ}) If two L-structures have the same domain then we say they are comparable. We say two comparable structures 𝔄 and 𝔅 are in the relation ≤_{Γ}, where Γ is a set of formulas in L, if the extension in 𝔄 of each formula in Γ is a subset of the extension of that formula in 𝔅.

In model theoretic terms, the consequences of second order circumscription are the sentences true in all minimal models under this pre-order ≤_{Γ}. This is now the most common form of circumscription.

0.5 Other Modifications of Circumscription

0.5.1 Hintikka

Hintikka[Hin88] suggests model minimization as an alternative to domain circumscription. Rather than prefer one model to another when the second is a sub-model of the first, he suggests that one model be preferred to another when the first is isomorphic to a sub-model of the second. This is essentially the notion of varying all predicates in domain circumscription. Lorenz[Lor94] calls this variable domain circumscription. Doherty, Lukaszewicz and Szalas[DLS96] suggest an extension, general domain circumscription, where subsets of the predicates functions and constants are allowed to vary.

0.5.2 Bossu and Siegel

Bossu and Siegel[BS84] proposed a treatment of non-monotonicity which is similar to circumscription. There are two notable differences however. Firstly they restrict themselves to minimizing every predicate symbol. Secondly, and more importantly, they change the notion of non-monotonic consequence. Rather than looking at the sentences that are true in all minimal models, they look at the sentences that are true at some model, and in all smaller models. In this way they drop the restriction that minimal models must exist.

0.5.3 Shoham

Shoham[Sho88] suggests that non-monotonic reasoning can be characterized by defining the sentences non-monotonically entailed by a theory as those sentences that are true in the minimal models of that theory, under some partial order. He considered other languages not just first order logic, and he considered arbitrary partial orders, not just those defined by circumscription policies. This work has been greatly extended in the study of non-monotonic consequence relations, [Gab85, KLM90, Mak89, Mak94] and others, an area outside the remit of this paper.

0.5.4 Rathmann, Winslett and Manasse

Rathmann, Winslett and Manasse[RWM90, RWM94] introduce a form of circumscription that they call structural circumscription. It is similar in model theoretic terms to classical circumscription, save that it redefines the notion of ≤ on the models of a sentence α. One model 𝔐 is ≤ a model 𝔑 is there is a homomorphism h, a function from the domain U_{1} of 𝔑 to the domain U of 𝔐, that satisfies the following conditions:

• The mapping h preserves functions constants and predicates that are not varied. If f is function, predicate or constant symbol from α’s signature, with extensions f_{𝔐} and f_{𝔑} in 𝔐 and 𝔑, we require that:

∀a_{1}, …, a_{n} ∈ U_{1}.h(f_{𝔑}(a_{1}, …, a_{n})) = f_{𝔐}(h(a_{1}), …, h(a_{n}))

Where n is the appropriate arity for each predicate and function, and is 0 for constants.

• The truth of minimized formulas is preserved. If γ is a minimized n-ary formula with extensions γ_{𝔐} and γ_{𝔑}, in 𝔐 and 𝔑, with n object variable and m predicate variables, then

∀a_{1}, …, a_{n} ∈ U_{1}b_{1}, …, b_{m} ∈ 2^{U_{1}}.γ_{𝔑}(a_{1}, …, a_{n}, b_{1}, …, b_{m}) →

γ_{𝔐}(h(a_{1}), …, h(a_{n}), h(b_{1}), …, h(b_{m}))

This defines a pre-order, and the consequences of the structural circumscription of a sentence α minimizing γ_{1}, …, γ_{n}, varying \overline{Q}, \overline{F}, \overline{C}, written StrCirc(α; γ_{1}, …, γ_{n}; \overline{Q}, \overline{F} , \overline{C}) are the sentences true in all minimal models under the preorder ≤.

Structural circumscription does achieve maximally unique names. However it also affects that part of the domain of objects that is not referred to by closed terms. This is not warranted by the original definition of the unique names assumption.

A second problem with structural circumscription is that it does not allow equality to be varied. This can be avoided by changing the semantics, as proposed by Rathmann et al.[RWM94], but then the original ideas of Goguen and Burstall’s[GB85] initial models are lost. The preferred models are no longer the initial models of the theory, as preference is no longer defined in terms of homomorphisms, but rather in terms of a binary relation which they call a generalized homomorphism.

0.5.5 Other Suggestions

Minker and Perlis[MP84] suggest protected circumscription, which modifies circumscription in an analogous way to allowing predicates to be varied. Perlis[Per87] looks at how circumscription can be described in the language of set-theory rather than second order logic. Auto-circumscription,[Per88] is a version of circumscription that provides for negative introspection. Lifschitz[Lif89b] also considers this question. The modifications we suggest are also appropriate in these cases.

Non-recursive circumscription[Mot87] builds on Minker and Perlis’s variable circumscription[PM86]. It weakens the circumscription formula so that it can no longer map satisfiable theories to unsatisfiable theories. We recognize that this is an important issue, but again this question lies outside the scope of this paper. Besnard, Moinard, and Mercer[BMM89] stress the importance of the extra expressive power that full circumscription gives over non-recursive circumscription.

Lifschitz[Lif86] explores the connection between logic programming and circumscription using a new variant, called pointwise circumscription. Its novelties include a weakening of circumscription, so that models are connected, in that the minimal models can be reached by changing instances of a predicate from true to false at a “point”. More importantly, it introduces a richer language for describing preferences. This work has been extended in the framework of regular circumscription[Lif89a].

References

[Ama68] Saul Amarel. On representations of problems of reasoning about actions. In Donald Michie, editor, Machine Intelligence 3, volume 3, pages 131–171. Elsevier/North-Holland, Amsterdam, London, New York, 1968.

[BMM89] P. Besnard, Y. Moinard, and R. E. Mercer. The Importance of Open and Recursive Circumscription. Artificial Intelligence, 39(2):251–262, 1989.

[BS84] G. Bossu and P. Siegel. Saturation, nonmonotonic reasoning, and the closed world assumption. Artificial Intelligence, 25(1):13–64, 1984.

[Dav80] M. Davis. The mathematics of non-monotonic reasoning. Artificial Intelligence, 13(1–2):73–80, 1980.

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

[DLS96] P. Doherty, W. Lukaszewicz, and A. Szalas. General Domain Circumscription and its First-Order Reduction. Technical Report LiTH-IDA-R-01, Linköping University, January 1996.

[EM87] D. W. Etherington and R. E. Mercer. Domain circumscription: A reevaluation. Computational Intelligence, 3(2):94–99, 1987.

[Gab85] D. Gabbay. Theoretical Foundations for Non-Monotonic Reasoning in Expert-Systems. In K. R. Apt, editor, Logics and Models of Concurrent systems, pages 439–458. Springer Verlag, 1985.

[GB85] J. A. Goguen and R. M. Burstall. Institutions: Abstract model theory for computer science. Technical Report CSLI-85-30, Center for Study of Language Logic and Information, Stanford, 1985.

[Hin88] J. Hintikka. Model minimization - an alternative to circumscription. Journal of Automated Reasoning, 4:1–13, 1988.

[KLM90] S. Kraus, D. Lehmann, and M. Magidor. Nonmonotonic Reasoning, Preferential Models and Cumulative Logics. Artificial Intelligence, 44(1):167–207, 1990.

[Lif85] V. Lifschitz. Computing Circumscription. In Proc. Ninth International Joint Conference on Artificial Intelligence (IJCAI ’85), pages 121–127, 1985.

[Lif86] V. Lifschitz. Pointwise Circumscription. In Proc. National Conference on Artificial Intelligence (AAAI ’86), pages 406–410, 1986.

[Lif89a] V. Lifschitz. Circumscriptive theories: a logic-based framework for knowledge representation. In Richmond Thomason, editor, Philosophical Logic and Artificial Intelligence, pages 109–160. Kluwer, 1989.

[Lif89b] Vladimir Lifschitz. Between circumscription and autoepistemic logic. In R. J. Brachman and H. J. Levesque, editors, Proceedings of the First International Conference on Principles of Knowledge Representation and Reasoning, pages 235– 244, Toronto, Ontario, 15-18 May 1989. Morgan Kaufmann.

[Lor94] S. Lorenz. A Tableuau Prover for Domain Minimization. Journal of Automated Reasoning, 13:375–390, 1994.

[Mak89] D. Makinson. General Theory of Cumulative Inference. In Reinfrank, de Kleer, Ginsberg, and Sandewall, editors, Non-Monotonic Reasoning, pages 1–18. Lecture Notes in Artificial Intelligence 346, Springer-Verlag, Jan 1989.

[Mak94] D. Makinson. General patterns in nonmonotonic reasoning. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume Vol. 3, Nonmonotonic and Uncertain Reasoning, pages 35–110. Oxford University Press, 1994.

[McC77] J. McCarthy. Epistemological Problems of Artificial Intelligence. In Proc. Fifth International Joint Conference on Artificial Intelligence (IJCAI ’77), pages 223– 227, Cambridge, MA, 1977.

[McC80] J. McCarthy. Circumscription - a Form of Non-Monotonic Reasoning. Artificial Intelligence, 13(1 and 2):27–39, 1980.

[McC86] J. McCarthy. Applications of Circumscription to Formalizing Commonsense Knowledge. Artificial Intelligence, 28:89–116, 1986.

[Mot87] P. L. Mott. A theorem on the Consistency of Circumscription. Artificial Intelligence, 31:87–98, 1987.

[MP84] J. Minker and D. Perlis. Protected circumscription. In Proc Workshop on Non-Monotonic Reasoning, pages 337–343, New Platz, 1984.

[Per87] D. Perlis. Circumscribing with Sets. Artificial Intelligence, 31:201–211, 1987.

[Per88] D. Perlis. Autocircumscription. Artificial Intelligence, 36:223–236, 1988.

[PM86] D. Perlis and J. Minker. Completeness Results for Circumscription. Artificial Intelligence, 28:29–42, 1986.

[Rei87] R. Reiter. Nonmonotonic reasoning. Annual Reviews of Computer Science, pages 147–188, 1987.

[RWM90] Peter K. Rathmann, Marianne Winslett, and Mark Manasse. Equality and circumscription. Technical Report 1615, Department of Computer Science, University of Illinois at Urbana-Champaign, Urbana, Illinois, 1990.

[RWM94] P. K. Rathmann, M. Winslett, and M. Manasse. Circumscription with homomorphisms: Solving the equality and counterexample problem. Journal of the ACM, 41(5):819–873, September 1994.

[Sho88] Y. Shoham. Reasoning about Change. MIT Press, Cambridge, USA, 1988.