文章基本信息

标题：Undecidability of a weak version of MSO+U
本地全文：下载
作者：Sreejith, A. V. ; Penelle, Vincent ; Guillon, Bruno 等
期刊名称：Logical Methods in Computer Science
印刷版ISSN：1860-5974
电子版ISSN：1860-5974
出版年度：2020
卷号：16
期号：1
页码：1-15
语种：English
出版社：Technical University of Braunschweig
摘要：We prove the undecidability of MSO on ω-words extended with the second-order predicate U1(X) which says that the distance between consecutive positions in a set X⊆N is unbounded. This is achieved by showing that adding U1 to MSO gives a logic with the same expressive power as MSO+U, a logic on ω-words with undecidable satisfiability. As a corollary, we prove that MSO on ω-words becomes undecidable if allowing to quantify over sets of positions that are ultimately periodic, i.e., sets X such that for some positive integer p, ultimately either both or none of positions x and x+p belong to X.
关键词：Computer Science ;Logic in Computer Science