Marvin Minsky challenged us advocates of formal systems based on mathematical logic to express the facts and nonmonotonic reasoning concerning the ability of birds to fly.
There are many ways of nonmonotonically axiomatizing the facts about which birds can fly. The following axioms using ab seem to me quite straightforward.
Unless an object is abnormal in aspect1, it can't fly. (We're using
a convention that parentheses may be omitted for functions and
predicates of one argument, so that (2) is the same as
.)
It wouldn't work to write 
instead of 
,
because we don't want a bird that is abnormal with respect to its ability
to fly to be automatically abnormal in other respects. Using aspects limits
the effects of proofs of abnormality.
Unless a bird is abnormal in aspect2, it can fly.
A bird is abnormal in aspect1, so (2) can't be used to show it can't fly. If (3) were omitted, when we did the circumscription we would only be able to infer a disjunction. Either a bird is abnormal in aspect1 or it can fly unless it is abnormal in aspect2. (3) expresses our preference for inferring that a bird is abnormal in aspect1 rather than aspect2. We call (3) a cancellation of inheritance axiom.
Ostriches are abnormal in aspect2. This doesn't say that an ostrich cannot fly -- merely that (4) can't be used to infer that it does. (5) is another cancellation of inheritance axiom.
Penguins are also abnormal in aspect2.
Normally ostriches and penguins can't fly. However, there is an out. (7) and (8) provide that under unspecified conditions, an ostrich or penguin might fly after all. If we give no such conditions, we will conclude that an ostrich or penguin can't fly. Additional objects that can fly may be specified. Each needs two axioms. The first says that it is abnormal in aspect1 and prevents (2) from being used to say that it can't fly. The second provides that it can fly unless it is abnormal in yet another way. Additional non-flying birds can also be provided for at a cost of two axioms per kind.
We haven't yet said that ostriches and penguins are birds, so let's do that and throw in that canaries are birds also.
Asserting that ostriches, penguins and canaries are birds will help inherit other properties from the class of birds. For example, we have
So far there is nothing to prevent ostriches, penguins and canaries from overlapping. We could write disjointness axioms like
but we require 
of them if we have n species.
It is more efficient to write axioms like
which makes the n species disjoint with only n axioms assuming that the distinctness of the names is apparent to the reasoner. This problem is like the unique names problem.
If these are the only facts to be taken into account, we
must somehow specify that what can fly is to be determined
by circumscribing the wff 
using ab and flies as variables.
Why exactly these? If ab were not taken as variable, couldn't
vary either, and the minimization problem would go away. Since
the purpose of the axiom set is to describe what flies, the predicate
flies must be varied also. Suppose we contemplate taking bird as
variable also. In the first place, this violates an intuition that
deciding what flies follows deciding what is a bird in the common
sense situations we want to cover. Secondly, if we use exactly the
above axioms and admit bird as a variable, we will further conclude
that the only birds are penguins, canaries and ostriches. Namely,
for these entities something has to be abnormal, and therefore minimizing
will involve making as few entities as possible penguins, canaries
and ostriches. If we also admit penguin, ostrich, and canary as
variable, we will succeed in making always false, and there will be
no birds at all.
However, if the same circumscriptions are done with additional
axioms like 
and 
, we will get the
expected result that Tweety can fly and Joe cannot even if all the
above are variable.
While this works it may be more straightforward, and therefore less likely to lead to subsequent trouble, to circumscribe birds, ostriches and penguins with axioms like
We have not yet specified how a program will know what to circumscribe. One extreme is to build it into the program, but this is contrary to the declarative spirit. However, a statement of what to circumscribe isn't just a sentence of the language because of its nonmonotonic character. Another possibility is to include some sort of metamathematical statement like
in a ``policy'' database available to the program. (16) is
intended to mean that is to be circumscribed with ab, flies,
bird, ostrich and penguin taken as variable. Explicitly listing
the variables makes adding new kinds awkward, since they will have
to be mentioned in the circumscribe statement. Section 11 on simple
abnormality theories presents yet another possibility.
