Fritz Henglein, Hans Lei\ss. Quasi-Monadic Semi-Unification Is Decidable. In Proc. Workshop on Unification (UNIF), Leeds, England, July 1990.
Download paper:
Adobe portable document (pdf)
Copyright notice:This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
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
@InProceedings{hele90,
Author = {Henglein, Fritz and Lei\ss, Hans},
Title = {Quasi-Monadic Semi-Unification Is Decidable},
BookTitle = {Proc. Workshop on Unification (UNIF)},
Address = {Leeds, England},
Month = {July},
Year = {1990}
}
Get EndNote Reference (.ref)