The Two-variable Fragment with Counting 4.1 Normal Forms

The main result of this chapter is that the satisfiability and finite satisfiability problems for this logic are both NExpTime-complete.