%0 Conference Proceedings
%F hele90
%A Henglein, Fritz
%A Lei\ss, Hans
%T Quasi-Monadic Semi-Unification Is Decidable
%B Proc. Workshop on Unification (UNIF)
%C Leeds, England
%X Semi-unification is a generalization of both unification and matching with applications in proof theory, term rewriting systems, polymorphic type inference, and natural language processing. It is the problem of solving a set of term inequalities M1 ≤ N1, . . . , Mk ≤ Nk , where ≤ is interpreted as the subsumption preordering on (first-order) terms. The general problem has been shown to be undecidable. As one of several special classes left-linear semi-unification, a generalization of monadic semi-unification has been shown to be efficiently decidable, though. In this paper we extend the decidability result for monadic semi-unification by permitting polyadic terms that are restricted, however, to contain occurrences of at most one variable. This is a generalization of monadic semi-unification that is essentially orthogonal to the left-linearity extension
%U http://www.diku.dk/hjemmesider/ansatte/henglein/papers/henglein1990a.pdf
%8 July
%D 1990