首页    期刊浏览 2024年11月10日 星期日
登录注册

文章基本信息

  • 标题: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
国家哲学社会科学文献中心版权所有