A corpus of syntactic and semantic analyses of transcribed
utterances from the OVIS domain was created to test this model. The
OVIS tree-bank currently contains 10.000 analyzed utterances. The
top-node semantics of each annotated utterance is an
*update-expression* that conforms to the formalism described
in Veldhuijzen van Zanten (1996). The semantic label of a node *N* in an analysis
consists of a rule, that indicates how the meaning of *N* (the
*update*) is built-up out of the meanings of *N*'s daughter
nodes. This semantic rule is typed. Its type follows from both the
rule itself, and from the types of the semantic labels of the
daughter-nodes of *N*, given the definition of the logical language
used. In the present case, the type of an expression is a pair of
integers, its *meet* and *join*. The *meet* and
*join* correspond to the *least upper bound* and the
*greatest lower bound* of the expression in the type-hierarchy,
as described in Veldhuijzen van Zanten (1996).

A semantically enriched STSG as described above, must fulfil an
important property. It has to be possible to define a function from
derivations to logical formulas, that is defined for *every*
derivation that can be produced by the grammar. In other words, the
information provided by semantic types and syntactic categories in an
analysis must be sufficient. Because the set of subtrees is closed
under the operation of subtree extraction, i.e., all subtrees *T*'
that can be extracted from another subtree *T*, belong to the same set
as *T*, it is easy to establish this property, even for a very large
grammar. We only need to look at the subtrees of depth one. If there
is a unique semantic rule associated with the root-node of all
subtrees of depth one, given the syntactic categories and semantic
types of its nodes, it follows that we know the semantic rule at the
nonterminal-nodes of every subtree. Fortunately, the nature of the
annotated tree-bank is such, that in about 99.9 % of cases we can
indeed establish the semantic rule at the root-node of a subtree in
this way. The few exceptions are assigned an ``exception-type'', to
reduce the uncertainty to zero. We exploit the property described
above, to construct a rewrite system for the semantic STSG. This
rewrite system applies the semantic rules associated with every node
in a derivation in a bottom up fashion, and arrives at the complete
logical formula.