In this section we informally describe the Earley
deduction method introduced in [Pereira and Warren1983]. Earley
deduction is a proof procedure for definite clauses and is named after
Earley's context-free parsing algorithm. As in Earley's original
algorithm, in Earley deduction the processing of definite
clauses is split into two basic deduction steps or rules of
inference, namely prediction and
completion
, dealing
respectively with top-down predictions of new clauses and bottom-up
combination of existing clauses. The results of prediction and completion (the
derived clauses) are lemmas, i.e., logical consequences of the program.
Earley deduction operates on two sets of definite clauses, called the
program and the state. In our case the program just
represents the grammar and lexicon and remains fixed. The state set,
on the other hand, will be continually augmented with new lemmas.
Whenever a new non-unit lemma is added, one of its negative literals is
selected (for example, when using the basic Prolog strategy, the
selected element would always be the leftmost literal in the body of a
lemma).
The prediction rule operates on non-unit lemmas, which we also call
active lemmas. This rule selects an active lemma B from the current
state and searches for a program clause C whose positive literal
(i.e., the head of C) unifies with the selected literal of B. If
this is possible the thereby derived clause 
is added to the
state set, where 
is the most general unifier of the two
literals. The selected element of B is said to instantiate the
program clause C to , or in other words, the selected
element has been used to predict an instantiation of C. Clearly,
prediction thus described realizes the top-down step of Earley
deduction.
The completion rule operates on unit lemmas, which we also call
passive lemmas. An active lemma C is chosen from the current state set,
whose selected element unifies with the passive lemma, which (if
possible) yields a new resolvent 
, where C' is C minus
its selected element. Since the completor actually reduces the number
of the negative literals of an active lemma, repeated application of
the completion rule eventually creates passive lemmas. Note that
completion against the selected literal is sufficient, because if a
completion with some other literal of the body is required, any
selection function will sooner or later come to this literal, because
the selection function will have to select from fewer and fewer
literals (see also [Pereira and Shieber1987], page 199). Hence, the
completor is also said to reduce C to or in other
words, the completion step (partially) completes derived clauses, in a
bottom-up fashion.
In [Pereira and Shieber1987] it is shown that the more specific constraints of context-free parsing allow a simplification that we cannot take advantage of here. In Earley's parsing algorithm, derived clause creation proceeds strictly from left to right. This means that any passive lemma needed to resolve against some active lemma is guaranteed to be constructed after the active lemma is created. Therefore, to perform all the pertinent resolutions, the algorithm need only look for active lemmas at the time when a passive lemma is created. However, a general Earley deduction proof procedure cannot guarantee this, so it is necessary to apply the completor also when active lemmas are created. As we will show, this is specifically the case for generation, because the structure of the input is not a sequence but a tree-like structure. In the implementation described in the next sections, we will separate these two cases into two inference rules, called passive-completion and active-completion, respectively.