Paper Info
Title
Two-variable Logic with Counting and a Linear Order.
Abstract
We study the finite satisfiability problem for the two-variable fragment offirst-order logic extended with counting quantifiers (C2) and interpreted overlinearly ordered structures. We show that the problem is undecidable in thecase of two linear orders (in the presence of two other binary symbols). In thecase of one linear order it is NEXPTIME-complete, even in the presence of thesuccessor relation. Surprisingly, the complexity of the problem explodes whenwe add one binary symbol more: C2 with one linear order and in the presence ofother binary predicate symbols is equivalent, under elementary reductions, tothe emptiness problem for multicounter automata.
Year
DOI
Venue
2016
10.4230/LIPIcs.CSL.2015.631
Logical Methods in Computer Science
DocType
Volume
Issue
Journal
12
2
ISSN
Citations 
PageRank 
Logical Methods in Computer Science, Volume 12, Issue 2 (August 11, 2016) lmcs:1640
0
0.34
References 
Authors
0
2
Name
Order
Citations
PageRank
witold charatonik134928.71
Piotr Witkowski2134.09