文章基本信息

标题：Two-Variable Universal Logic with Transitive Closure
本地全文：下载
作者：Emanuel Kieronski ; Jakub Michaliszyn
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2012
卷号：16
页码：396-410
DOI：10.4230/LIPIcs.CSL.2012.396
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：We prove that the satisfiability problem for the two-variable, universal fragment of first-order logic with constants (or, alternatively phrased, for the Bernays-Schönfinkel class with two universally quantified variables) remains decidable after augmenting the fragment by the transitive closure of a single binary relation. We give a 2-NExpTime-upper bound and a 2-ExpTime-lower bound for the complexity of the problem. We also study the cases in which the number of constants is restricted. It appears that with two constants the considered fragment has the finite model property and NExpTime-complete satisfiability problem. Adding a third constant does not change the complexity but allows to construct infinity axioms. A fourth constant lifts the lower complexity bound to TwoExpTime. Finally, we observe that we are close to the border between decidability and undecidability: adding a third variable or the transitive closure of a second binary relation lead to undecidability.
关键词：two-variable logic; transitive closure; decidability