Given the above procedures for computing ,
,
,
,
, and
, one can
now define a procedure for computing
.
This procedure takes a model M along with an event-logic expression
and computes a set of normalized spanning intervals that represents the
set I of intervals
for which
is true.
The model M is a set of atomic event-occurrence formulae of the form
, where
is a ground primitive
event-logic expression and
is a normalized spanning interval.
A model entry
indicates that the primitive event
occurred during all intervals in the extension of
.
The procedure performs structural induction on .
It computes a set of normalized spanning intervals to the represent the
occurrence of each atomic event-logic expression in
and recursively
combines the sets so computed for each child subexpression to yield the sets
for each parent subexpression.
An important property of this inference procedure is that for any finite
model M,
, the set I of intervals
for which
is
true, can be represented by a finite set of normalized spanning intervals.
Nominally, the number of normalized spanning intervals in
can be
exponential in the subexpression depth of
because each step in the
structural induction can introduce a constant factor growth in the size of the
set.
However, in practice, such exponential growth does not occur.
Computing
for all of the event types given in
Figure 10 for all of the movies that have been tried so
far have yielded sets of fewer than a dozen normalized spanning intervals.