joint work with Witold Charatonik and Emanuel Kieroński

The deterministic transitive closure operator, added to languages containing even only two variables, allows to express many
natural properties of a binary relation, including being a linear
order, a tree, a forest or a partial function. This makes it a
potentially attractive ingredient of computer science formalisms. We consider the extension of the two-variable fragment of
first-order logic by the deterministic transitive closure of a
single binary relation, and prove that the satisfiability and finite
satisfiability problems for the obtained logic are decidable and
EXPSPACE-complete. We also consider the class
of universal first-order formulas in prenex form.