Anzeige
Erschienen in:
2012 | OriginalPaper | Buchkapitel
New Algorithms for Unification Modulo One-Sided Distributivity and Its Variants
verfasst von : Andrew M. Marshall, Paliath Narendran
Erschienen in: Automated Reasoning
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
An algorithm for unification modulo
one-sided
distributivity is an early result by Tiden and Arnborg [14]. Unfortunately the algorithm presented in the paper, although correct, has recently been shown not to be polynomial time bounded as claimed [11]. In addition, for some instances, there exist most general unifiers that are exponentially large with respect to the input size. In this paper we first present a new polynomial time algorithm that solves the
decision
problem for a non-trivial subcase, based on a typed theory, of unification modulo one-sided distributivity. Next we present a new polynomial algorithm that solves the
decision
problem for unification modulo one-sided distributivity. A construction, employing string compression, is used to achieve the polynomial bound.