next up previous
Next: DOMAIN CIRCUMSCRIPTION Up: CIRCUMSCRIPTION-A FORM OF NONMONOTONIC Previous: MISSIONARIES AND CANNIBALS

THE FORMALISM OF CIRCUMSCRIPTION

Let A be a sentence of first order logic containing a predicate symbol tex2html_wrap_inline579 which we will write tex2html_wrap_inline465 . We write tex2html_wrap_inline467 for the result of replacing all occurrences of P in A by the predicate expression tex2html_wrap_inline473 . (As well as predicate symbols, suitable tex2html_wrap_inline475 -expressions are allowed as predicate expressions).

Definition. The circumscription of P in A(P) is the sentence schema

   equation50

(1) can be regarded as asserting that the only tuples tex2html_wrap_inline483 that satisfy P are those that have to -- assuming the sentence A. Namely, (1) contains a predicate parameter tex2html_wrap_inline473 for which we may subsitute an arbitrary predicate expression. (If we were using second order logic, there would be a quantifier tex2html_wrap_inline491 in front of (1).) Since (1) is an implication, we can assume both conjuncts on the left, and (1) lets us conclude the sentence on the right. The first conjunct tex2html_wrap_inline467 expresses the assumption that tex2html_wrap_inline473 satisfies the conditions satisfied by P, and the second tex2html_wrap_inline499 expresses the assumption that the entities satisfying tex2html_wrap_inline473 are a subset of those that satisfy P. The conclusion asserts the converse of the second conjunct which tells us that in this case, tex2html_wrap_inline473 and P must coincide.

We write tex2html_wrap_inline623 if the sentence q can be obtained by deduction from the result of circumscribing P in A. As we shall see tex2html_wrap_inline631 is a nonmonotonic form of inference, which we shall call circumscriptive inference.

A slight generalization allows circumscribing several predicates jointly; thus jointly circumscribing P and Q in A(P,Q) leads to

  displaymath525

in which we can simultaneously substitute for tex2html_wrap_inline473 and tex2html_wrap_inline529 . The relation tex2html_wrap_inline645 is defined in a corresponding way. Although we don't give examples of joint circumscription in this paper, we believe it will be important in some AI applications.

Consider the following examples:

Example 1. In the blocks world, the sentence A may be

  equation85

asserting that A, B and C are blocks. Circumscribing isblock in (2) gives the schema

  equation89

If we now substitute

  equation95

into (3) and use (2), the left side of the implication is seen to be true, and this gives

  equation100

which asserts that the only blocks are A, B and C, i.e. just those objects that (2) requires to be blocks. This example is rather trivial, because (2) provides no way of generating new blocks from old ones. However, it shows that circumscriptive inference is nonmonotonic since if we adjoin tex2html_wrap_inline663 to (2), we will no longer be able to infer (5).

Example 2. Circumscribing the disjunction

  equation108

leads to

  equation111

We may then substitute successively tex2html_wrap_inline563 and tex2html_wrap_inline565 , and these give respectively

  equation117

which simplifies to

  equation120

and

  equation123

which simplifies to

  equation126

(9), (11) and (6) yield

  equation132

which asserts that either A is the only block or B is the only block.

Example 3. Consider the following algebraic axioms for natural numbers, i.e., non-negative integers, appropriate when we aren't supposing that natural numbers are the only objects.

  equation136

Circumscribing isnatnum in (13) yields

  equation140

(14) asserts that the only natural numbers are those objects that (13) forces to be natural numbers, and this is essentially the usual axiom schema of induction. We can get closer to the usual schema by substituting tex2html_wrap_inline587 . This and (13) make the second conjunct drop out giving

  equation146

Example 4. Returning to the blocks world, suppose we have a predicate on(x,y,s) asserting that block x is on block y in situation s. Suppose we have another predicate above(x,y,s) which asserts that block x is above block y in situation s. We may write

  equation150

and

  equation153

i.e. above is a transitive relation. Circumscribing above in (16) tex2html_wrap_inline615 (17) gives

  equation158

which tells us that above is the transitive closure of on.

In the preceding two examples, the schemas produced by circumscription play the role of axiom schemas rather than being just conjectures.


next up previous
Next: DOMAIN CIRCUMSCRIPTION Up: CIRCUMSCRIPTION-A FORM OF NONMONOTONIC Previous: MISSIONARIES AND CANNIBALS

John McCarthy
Tue May 14 00:04:52 PDT 1996