Ptime canonization for two variables with counting
Martin Otto · 2002
We consider infinitary logic with two variable symbols and counting quantifiers, C/sup 2/, and its intersection with PTIME on finite relational structures. In particular we exhibit a PTIME canonization procedure for finite relational structures which provides unique representatives up to equivalence in C/sup 2/. As a consequence we obtain a recursive presentation for the class of all those queries on arbitrary finite relational structures which are both PTIME and definable in C/sup 2/. The proof renders a succinct normal form representation of this non-trivial semantically defined fragment of PTIME. Through specializations of the proof techniques similar results apply with respect to the logic L/sup 2/, infinitary logic with two variable symbols, itself.