Sorted Unification and its Applications to Automated Theorem Proving (Extended Abstract)

) Christoph Weidenbach Max-Planck-Institut fur Informatik Im Stadtwald, 66123 Saarbrucken, Germany email: weidenb@mpi-sb.mpg.de phone: +49-681-9325221 fax: +49-681-9325299 June 21, 1996 1 Introduction The task of unification is always the search for a substitution oe for a unification problem t ß s such that toe = soe. For example, the standard 1 unification problem x ß f(y) has the obvious standard solution oe = fx=f(y)g. In the presence of sort theories 2 , we attach sorts to the variables and require, in addition to standard unification, that the assignments of oe respect the sort restrictions. For example, consider the sort theory 3 L = fS(f(g(x fSg ))); T (f(y fTg )); T (g(y fTg )); S(a); T(a)g and a modification of the above unification problem where we have attached sorts to the variables. x fS;Tg ß f(y fTg ) In our approach, sorts are sets of monadic predicates. The denotation of the monadic predicates is fixed by the sort theory and sorts restrict the domain of vari..