文章基本信息

标题：Two-Restricted One Context Unification is in Polynomial Time
本地全文：下载
作者：Adri{\`a} Gasc{\'o}n ; Manfred Schmidt-Schau{\ss ; Ashish Tiwari 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2015
卷号：41
页码：405-422
DOI：10.4230/LIPIcs.CSL.2015.405
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：One Context Unification (1CU) extends first-order unification by introducing a single context variable. This problem was recently shown to be in NP, but it is not known to be solvable in polynomial time. We show that the case of 1CU where the context variable occurs at most twice in the input (1CU2r) is solvable in polynomial time. Moreover, a polynomial representation of all solutions can also be computed in polynomial time. The 1CU2r problem is important as it is used as a subroutine in polynomial time algorithms for several more-general classes of 1CU problem. Our algorithm can be seen as an extension of the usual rules of first-order unification and can be used to solve related problems in polynomial time, such as first-order unification of two terms that tolerates one clash. All our results assume that the input terms are represented as Directed Acyclic Graphs.
关键词：context unification; first-order unification; deduction; type checking