文章基本信息

标题：FO^2 with one transitive relation is decidable
本地全文：下载
作者：Wieslaw Szwast ; Lidia Tendera
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2013
卷号：20
页码：317-328
DOI：10.4230/LIPIcs.STACS.2013.317
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：We show that the satisfiability problem for the two-variable first-order logic, FO^2, over transitive structures when only one relation is required to be transitive, is decidable. The result is optimal, as FO^2 over structures with two transitive relations, or with one transitive and one equivalence relation, are known to be undecidable, so in fact, our result completes the classification of FO^2-logics over transitive structures with respect to decidability. We show that the satisfiability problem is in 2-NExpTime. Decidability of the finite satisfiability problem remains open.
关键词：classical decision problem; two-variable first-order logic; decidability; computational complexity