You can also check my publications on DBLP and Google Scholar.

Sort by year

Conference Papers
Proceedings of the 37th IARCS Annual Conference on Foundations of
Software Technology and Theoretical Computer Science, FSTTCS 2017,
December 11–15, 2017, Kanpur, India. LIPIcs 93, Schloss Dagstuhl -
Leibniz-Zentrum fuer Informatik 2017, pages 12:1–12:16.

We consider the satisfiability problem for the two-variable fragment of the first-order logic extended with modulo counting quantifiers and interpreted over finite words or trees. We prove a small-model property of this logic, which gives a technique for deciding the satisfiability problem. In the case of words this gives a new proof of EXPSPACE upper bound, and in the case of trees it gives a 2EXPTIME algorithm. This algorithm is optimal: we prove a matching lower bound by a generic reduction from alternating Turing machines working in exponential space; the reduction involves a development of a new version of tiling games.

Conference Papers
Proceedings of the 26th EACSL Annual Conference on Computer Science
Logic, CSL 2017, August 20-24, 2017, Stockholm, Sweden. LIPIcs 82,
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik 2017, pages
11:1-11:20

The finite satisfiability problem for the two-variable fragment of first-order logic interpreted over trees was recently shown to be ExpSpace-complete. We consider two extensions of this logic. We show that adding either additional binary symbols or counting quantifiers to the logic does not affect the complexity of the finite satisfiability problem. However, combining the two extensions and adding both binary symbols and counting quantifiers leads to an explosion of this complexity. We also compare the expressive power of the two-variable fragment over trees with its extension with counting quantifiers. It turns out that the two logics are equally expressive, although counting quantifiers do add expressive power in the restricted case of unordered trees.

Conference Papers
Proceedings of ESSLLI 2017 Student Session, 29th European Summer
School in Logic, Language & Information, July 17-28, 2017,
Toulouse, France, pages 7-13

We consider the one-variable fragment of first-order logic extended with modulo counting quantifiers. We prove NPTime-completeness of such fragment by presenting an optimal algorithm for solving its finite satisfiability problem.

Bachelor Thesis
Dissertation advisor: prof. dr hab. Witold Charatonik, Date of
defence: Feb. 15, 2017

The finite satisfiability problem for the two-variable fragment of first-order logic interpreted over trees was recently shown to be ExpSpace-complete. We show that adding counting quantifiers to the logic does not affect the complexity of the finite satisfiability problem.