2012 | OriginalPaper | Chapter
New Algorithms for Unification Modulo One-Sided Distributivity and Its Variants
Authors : Andrew M. Marshall, Paliath Narendran
Published in: Automated Reasoning
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. 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.