• DocumentCode
    3298831
  • Title

    Two-variable logic with counting is decidable

  • Author

    Gräde, Erich ; Otto, Martin ; Rosen, Eric

  • Author_Institution
    Math. Grundlagen der Inf., Tech. Hochschule Aachen, Germany
  • fYear
    1997
  • fDate
    29 Jun-2 Jul 1997
  • Firstpage
    306
  • Lastpage
    317
  • Abstract
    We prove that the satisfiability and the finite satisfiability problems for C2 are decidable. C2 is first-order logic with only two variables in the presence of arbitrary counting quantifiers 3⩾m,m⩾1. It considerably extends L2 plain first-order with only two variables, which is known to be decidable by a result of Mortimer´s. Unlike L2, C2 does not have the finite model property
  • Keywords
    computability; decidability; formal logic; decidable; finite satisfiability; first-order logic; satisfiability; two-variable logic; Boolean functions; H infinity control; Logic; Page description languages; Research and development; Terminology; Vocabulary;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Logic in Computer Science, 1997. LICS '97. Proceedings., 12th Annual IEEE Symposium on
  • Conference_Location
    Warsaw
  • ISSN
    1043-6871
  • Print_ISBN
    0-8186-7925-5
  • Type

    conf

  • DOI
    10.1109/LICS.1997.614957
  • Filename
    614957
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=3298831