Here is an annotated EKL proof that circumscribes the predicate
*e*(*x*,*y*) discussed in section 6.

What the user types is indicated by the numbered statements in lower case. What EKL types is preceded by semicolons at the beginning of each line and is in upper case. We omit EKL's type-out when it merely repeats what the command asked it to do, as in the commands DERIVE, ASSUME and DEFINE.

Since EKL does not have attachments to determine the equivalence of names, we establish a correspondence between the names in our domain and some natural numbers.

EKL does know about the distinctness of natural numbers, so this can be derived.

We have to tell EKL to use the properties of equality rather than regarding it as just another predicate symbol in order to do the next step. Sometimes this leads to combinatorial explosion.

This shows that two names themselves are distinct.

Here we use second order logic to define the notion of equivalence relation. The first word after ``define'' is the entity being defined and included between vertical bars is the defining relation. EKL checks that an entity satisfying the relation exists.

We define ax as a predicate we want our imitation equality to
satisfy. We have chosen a very simple case, namely making *a* and
*b* ``equal'' and nothing else.

This defines *ax*1 as the second order predicate specifying the
circumscription of *ax*.

We now specify that *e*0 satisfies *ax*1. It takes till step 17
to determine what *e*0 actually is. When EKL includes circumscription
as an operator, we may be able to write something like circumscribe(*e*0,*ax*1)
and make this step occur. For now it's just an ordinary assumption.

The predicate *e*2 defined here is what *e*0 will turn out to be.

Now EKL agrees that *e*2 is an equivalence relation. This step takes
the KL-10 about 14 seconds.

Moreover it satisfies ax.

A trivial step of expanding the definition of *ax*1. EKL tells us
that this fact depends on the assumption CIRCUM. So do many of
the subsequent lines of the proof, but we omit it henceforth to
save space.

The first conjunct of the previous step.

We expand *ax*(*e*0) according to the definitions of *ax* and *equiv*.

This is a fact of propositional calculus used as a rewrite rule in the next step. A program that can use circumscription by itself will either need to generate this step or systematically avoid the need for it.

This is the least obvious step, because rewrite by cases is used after some preliminary transformation of the formula.

DERIVE is substituting *e*2 for the variable *e*1 in step 11 and using
the fact *ax*(*e*2) and step 15 to infer the conclusion of the implication
that follows the quantifier

Expanding the definition of *e*2 tells us the final result of
circumscribing *e*0(*x*,*y*). A more complex *ax*(*e*0) -- see step 5 --
would give a more complex result upon circumscription. However, it
seems that the proof would be similar. Therefore, it could perhaps be
made into some kind of macro.

Sat Jun 1 13:54:22 PDT 1996