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

文章基本信息

  • 标题:Quantifier Alternation in Two-Variable First-Order Logic with Successor Is Decidable
  • 本地全文:下载
  • 作者:Manfred Kufleitner ; Alexander Lauser
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2013
  • 卷号:20
  • 页码:305-316
  • DOI:10.4230/LIPIcs.STACS.2013.305
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:We consider the quantifier alternation hierarchy within two-variable first-order logic FO^2[<,suc] over finite words with linear order and binary successor predicate. We give a single identity of omega-terms for each level of this hierarchy. This shows that for a given regular language and a non-negative integer~$m$ it is decidable whether the language is definable by a formula in FO^2[<,suc] which has at most m quantifier alternations. We also consider the alternation hierarchy of unary temporal logic TL[X,F,Y,P] defined by the maximal number of nested negations. This hierarchy coincides with the FO^2[<,suc] quantifier alternation hierarchy.
  • 关键词:automata theory; semigroups; regular languages; first-order logic
国家哲学社会科学文献中心版权所有