Logic in Computer Science, Symposium on (2013)

New Orleans, LA, USA USA

June 25, 2013 to June 28, 2013

ISSN: 1043-6871

ISBN: 978-1-4799-0413-6

pp: 73-82

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2013.12

ABSTRACT

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.

INDEX TERMS

Vegetation, Surgery, Vocabulary, Implants, Computer science, Data structures, Complexity theory, ranked tree, two-variable logic, counting quantifiers, satisfiability

CITATION

Witold Charatonik,
Piotr Witkowski,
"Two-Variable Logic with Counting and Trees",

*Logic in Computer Science, Symposium on*, vol. 00, no. , pp. 73-82, 2013, doi:10.1109/LICS.2013.12