Logic in Computer Science (LICS 1995)

Paper: Ptime Canonization for Two Variables with Counting (at LICS 1995)

Authors: Martin Otto

Abstract

We consider infinitary logic with two variable symbols and counting quantifiers 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 two variable infinitary logic with counting quantifiers. 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 two variable infinitary logic with counting quantifiers. 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 infinitary logic with two variable symbols and without counting quantifiers.

BibTeX

  @InProceedings{Otto-PtimeCanonizationfo,
    author = 	 {Martin Otto},
    title = 	 {Ptime Canonization for Two Variables with Counting},
    booktitle =  {Proceedings of the Tenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1995},
    year =	 1995,
    editor =	 {Dexter Kozen},
    month =	 {June}, 
    pages =      {342-352},
    location =   {San Diego, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }