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.