Logic in Computer Science, Symposium on (2013)
New Orleans, LA, USA USA
June 25, 2013 to June 28, 2013
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2013.12
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 C2 and 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 C2 is NEXPTIME-complete.
Vegetation, Surgery, Vocabulary, Implants, Computer science, Data structures, Complexity theory, ranked tree, two-variable logic, counting quantifiers, satisfiability
W. Charatonik and P. Witkowski, "Two-Variable Logic with Counting and Trees," Logic in Computer Science, Symposium on(LICS), New Orleans, LA, USA USA, 2013, pp. 73-82.