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

文章基本信息

  • 标题:The FO2 alternation hierarchy is decidable
  • 本地全文:下载
  • 作者:Manfred Kufleitner ; Pascal Weil
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2012
  • 卷号:16
  • 页码:426-439
  • DOI:10.4230/LIPIcs.CSL.2012.426
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:We consider the two-variable fragment FO2[<] of first-order logic over finite words. Numerous characterizations of this class are known. Therien and Wilke have shown that it is decidable whether a given regular language is definable in FO2[<]. From a practical point of view, as shown by Weis, FO2[<] is interesting since its satisfiability problem is in NP. Restricting the number of quantifier alternations yields an infinite hierarchy inside the class of FO2[<]-definable languages. We show that each level of this hierarchy is decidable. For this purpose, we relate each level of the hierarchy with a decidable variety of finite monoids. Our result implies that there are many different ways of climbing up the FO2[<]-quantifier alternation hierarchy: deterministic and co-deterministic products, Mal'cev products with definite and reverse definite semigroups, iterated block products with J-trivial monoids, and some inductively defined omega-term identities. A combinatorial tool in the process of ascension is that of condensed rankers, a refinement of the rankers of Weis and Immerman and the turtle programs of Schwentick, Therien, and Vollmer.
  • 关键词:first-order logic; regular language; automata theory; semigroup; ranker
国家哲学社会科学文献中心版权所有