A decision algorithm for stratified context unification

被引：18
|
作者：
Schmidt-Schauss, M [1 ]
机构：
[1] Goethe Univ Frankfurt, Fachbereich Informat, D-60054 Frankfurt, Germany
来源：
JOURNAL OF LOGIC AND COMPUTATION | 2002年 / 12卷 / 06期
关键词：
unification; constraint solving; automated deduction; context unification; string unification;
D O I：
10.1093/logcom/12.6.929
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Context unification is a variant of second-order unification and also a generalization of string unification. Currently it is not known whether context unification is decidable. An expressive fragment of context unification is stratified context unification. Recently, it turned out that stratified context unification and one-step rewrite constraints are equivalent. This paper contains a description of a decision algorithm SCU for stratified context unification together with a proof of its correctness, which shows decidability of stratified context unification as well as of satisfiability of one-step rewrite constraints.
引用
收藏
页码：929 / 953
页数：25
相关论文
共 50 条
  • [1] Dominance constraints in stratified context unification
    Erk, Katrin
    Niehren, Joachim
    [J]. INFORMATION PROCESSING LETTERS, 2007, 101 (04) : 141 - 147
  • [2] Stratified Context Unification is NP-complete
    Levy, Jordi
    Schmidt-Schauss, Manfred
    Villaret, Mateu
    [J]. AUTOMATED REASONING, PROCEEDINGS, 2006, 4130 : 82 - 96
  • [3] On the complexity of Bounded Second-Order Unification and Stratified Context Unification
    Levy, Jordi
    Schmidt-Schauss, Manfred
    Villaret, Mateu
    [J]. LOGIC JOURNAL OF THE IGPL, 2011, 19 (06) : 763 - 789
  • [4] A decision algorithm for distributive unification
    Schmidt-Schauss, M
    [J]. THEORETICAL COMPUTER SCIENCE, 1998, 208 (1-2) : 111 - 148
  • [5] Context unification with one context variable
    Gascon, Adria
    Godoy, Guillem
    Schmidt-Schauss, Manfred
    Tiwari, Ashish
    [J]. JOURNAL OF SYMBOLIC COMPUTATION, 2010, 45 (02) : 173 - 193
  • [6] Deciding Context Unification
    Jez, Artur
    [J]. JOURNAL OF THE ACM, 2019, 66 (06)
  • [7] Context Unification is in PSPACE
    Jez, Artur
    [J]. AUTOMATA, LANGUAGES, AND PROGRAMMING (ICALP 2014), PT II, 2014, 8573 : 244 - 255
  • [8] A DECISION MAKING ALGORITHM FOR CONSIDERING ECT IN THE CONTEXT OF DEMENTIA
    Ostroff, Robert
    Katz, Rachel
    [J]. JOURNAL OF ECT, 2019, 35 (03) : E25 - E25
  • [9] A fast inter mode decision algorithm based on the context
    School of Information Engineering, Wuhan University of Technology, WHUT, Wuhan, China
    [J]. Int. Conf. E-Bus. Inf. Syst. Secur., EBISS, (615-617):
  • [10] A Fast Inter Mode Decision Algorithm Based On the Context
    Wang, Yuanli
    Jiang, Gen
    Wang, Qinqin
    [J]. 2010 2ND INTERNATIONAL CONFERENCE ON E-BUSINESS AND INFORMATION SYSTEM SECURITY (EBISS 2010), 2010, : 615 - 617
12345