1. Suppose we have a data base of facts axiomatized by a formalism
involving the predicate ab. In connection with a particular problem, a
program takes a subcollection of these facts together with the specific
facts of the problem and then circumscribes 
. We get a second order
formula, and in general, as the natural number example of (McCarthy 1980)
shows, this formula is not equivalent to any first order formula.
However, many common sense domains are axiomatizable in such a way that
the circumscription is equivalent to a first order formula. In this case
we call the circumscription collapsible. For example, Vladimir Lifschitz
(1985) has shown that this is true if the axioms are from a certain class
he calls ``separable'' formulas. This can presumably be
extended to other cases in which the ranges and domains of the functions
are disjoint, so that there is no way of generating an infinity of
elements.
Circumscription is also collapsible when the predicates are all monadic and there are no functions.
2. We can then regard the process of deciding what facts to take into account and then circumscribing as a process of compiling from a slightly higher level nonmonotonic language into mathematical logic, especially first order logic. We can also regard natural language as higher level than logic. However, as I shall discuss elsewhere, natural language doesn't have an independent reasoning process, because most natural language inferences involve suppressed premisses which are not represented in natural language in the minds of the people doing the reasoning.
Reiter has pointed out, both informally and implicitly in (Reiter 1982) that circumscription often translates directly into Prolog program once it has been decided what facts to take into account.
3. Circumscription has interesting relations to Reiter's (1980a) logic of defaults. In simple cases they give the same results. However, a computer program using default logic would have to establish the existence of models, perhaps by constructing them, in order to determine that the sentences mentioned in default rules were consistent. Such computations are not just selectively applying the rules of inference of logic but are metamathematical. At present this is treated entirely informally, and I am not aware of any computer program that finds models of sets of sentences or even interacts with a user to find and verify such models.
Circumscription works entirely within logic as Appendices A and B illustrate. It can do this, because it uses second order logic to import some of the model theory of first order formulas into the theory itself. Finding the right substitution for the predicate variables is, in the cases we have examined, the same task as finding models of a first order theory. Putting everything into the logic itself is an advantage as long as there is neither a good theory of how to construct models nor programs that do it.
Notice, however, that finding an interpretation of a language has two parts -- finding a domain and interpreting the predicate and function letters by predicates and functions on the domain. It seems that the second is easier to import into second order logic than the first. This may be why our treatment of unique names is awkward.
4. We are only part way to our goal of providing a formalism in which a database of common sense knowledge can be expressed. Besides sets of axioms involving ab, we need ways of specifying what facts shall be taken into account and what functions and predicates are to be taken as variable.
Moreover, some of the circumscriptions have unwanted conclusions, e.g. that there are no ostriches if none are explicitly mentioned. Perhaps some of this can be fixed by introducing the notion of present situation. An axiom that ostriches exist will do no harm if what is allowed to vary includes only ostriches that are present.
5. Nonmonotonic formalisms in general, and circumscription in particular, have many as yet unrealized applications to formalizing common sense knowledge and reasoning. Since we have to think about these matters in a new way, what the applications are and how to realize them isn't immediately obvious. Here are some suggestions.
When we are searching for the ``best'' object of some kind, we often jump to the conclusion that the best we have found so far is the best. This process can be represented as circumscribing better(x,candidate), where candidate is the best we have found so far. If we attempt this circumscription while including certain information in our axiom A(better,P), where P represents additional predicates being varied, we will succeed in showing that there is nothing better only if this is consistent with the information we take into account. If the attempt to circumscribe fails, we would like our reasoning program to use the failure as an aid to finding a better object. I don't know how hard this would be.