The truth-conditional semantics of the DRS language is given by defining when an embedding function verifies a DRS in a given model. An embedding function is a partial mapping from discourse referents to individuals. Given two embedding functions f and g and a DRS K, we say that g extends f with respect to K, or f[K]g for short, iff Dom(g) = Dom(f) ∪ UK, and for all x in Dom(f): f(x) = g(x).  Viewing functions as set-theoretic objects, this can be formulated more succinctly as follows: 