@TechReport{	  KufleitnerL13tr,
  author	= "Manfred Kufleitner and Alexander Lauser",
  title		= "Nesting Negations in $\mathrm{FO}^{2}$ over Finite Words",
  institution	= "University of Stuttgart",
  pages		= "19",
  type		= "Technical Report Computer Science",
  number	= "2013/07",
  month		= "9",
  year		= "2013",
  keywords	= "regular language; finite monoid; positive variety;
		  first-order logic",
  language	= "English",
  address	= "University of Stuttgart, Institute of Formal Methods in
		  Computer Science, Theoretical Computer Science",
  abstract	= "We consider the fragment $\Sigma^{2}_{m}$ of two-variable
		  first-order logic $\mathrm{FO}^{2}[<]$ over finite words
		  which is defined by restricting the nesting depth of
		  negations to at most m. Our first result is a combinatorial
		  characterization of $\Sigma^{2}_{m}$ in terms of so-called
		  rankers. This generalizes a result by Weis and Immerman
		  which we recover as an immediate consequence.
		  
		  Our second result is an effective algebraic
		  characterization of $\Sigma^{2}_{m}$, i.e., for every
		  integer m one can decide whether a given regular language
		  is definable by a two-variable first-order formula with
		  negation nesting depth at most m. More precisely, for every
		  $m$ we give omega-terms $U_{m}$ and $V_{m}$ such that an
		  $\mathrm{FO}^{2}$-definable language is in $\Sigma^{2}_{m}$
		  if and only if its ordered syntactic monoid satisfies the
		  identity $U_{m} \le V_{m}$."
}