Regular Typed Unification

Here we define a new unification algorithm for terms interpreted in semanticdomains denoted by a subclass of regular types here called deterministicregular types. This reflects our intention not to handle the semantic universeas a homogeneous collection of values, but instead, to partition it in a waythat is similar to data types in programming languages. We first define the newunification algorithm which is based on constraint generation and constraintsolving, and then prove its main properties: termination, soundness, andcompleteness with respect to the semantics. Finally, we discuss how to applythis algorithm to a dynamically typed version of Prolog.