Two-Variable Logic with Counting and Trees
Witold Charatonik, Piotr Witkowski · 2013
We consider the two-variable logic with counting quantifiers (C2) interpreted over finite structures that contain two forests of ranked trees. This logic is strictly more expressive than standard C2and it is no longer a fragment of the first order logic. In particular, it can express that a structure is a ranked tree, a cycle or a connected graph of bounded degree. It is also strictly more expressive than the first-order logic with two variables and two successor relations of two finite linear orders. We give a decision procedure for the satisfiability problem for this logic. The procedure runs in NEXPTIME, which is optimal since the satisfiability problem for plain C2is NEXPTIME-complete.