Two-Variable Universal Logic with Transitive Closure

Authors Emanuel Kieronski, Jakub Michaliszyn

Thumbnail PDF


  • Filesize: 465 kB
  • 15 pages

Document Identifiers

Author Details

Emanuel Kieronski
Jakub Michaliszyn

Cite AsGet BibTex

Emanuel Kieronski and Jakub Michaliszyn. Two-Variable Universal Logic with Transitive Closure. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 396-410, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


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


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads