Blog
About

7
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: not found

      On the Decision Problem for Two-Variable First-Order Logic

      , ,

      Bulletin of Symbolic Logic

      JSTOR

      Read this article at

      ScienceOpenPublisher
      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          We identify the computational complexity of the satisfiability problem for FO2, the fragment of first-order logic consisting of all relational first-order sentences with at most two distinct variables. Although this fragment was shown to be decidable a long time ago, the computational complexity of its decision problem has not been pinpointed so far. In 1975 Mortimer proved that FO2has thefinite-model property, which means that if an FO2-sentence is satisiable, then it has a finite model. Moreover, Mortimer showed that every satisfiable FO2-sentence has a model whose size is at most doubly exponential in the size of the sentence. In this paper, we improve Mortimer's bound by one exponential and show that every satisfiable FO2-sentence has a model whose size is at most exponential in the size of the sentence. As a consequence, we establish that the satisfiability problem for FO2is NEXPTIME-complete.

          Related collections

          Most cited references 22

          • Record: found
          • Abstract: not found
          • Article: not found

          The complexity of propositional linear temporal logics

           A. Sistla,  E. Clarke (1985)
            Bookmark
            • Record: found
            • Abstract: not found
            • Article: not found

            Knowledge and common knowledge in a distributed environment

              Bookmark
              • Record: found
              • Abstract: not found
              • Article: not found

              An optimal lower bound on the number of variables for graph identification

                Bookmark

                Author and article information

                Journal
                applab
                Bulletin of Symbolic Logic
                Bull. symb. log.
                JSTOR
                1079-8986
                1943-5894
                March 1997
                January 2014
                : 3
                : 01
                : 53-69
                Article
                10.2307/421196
                © 1997

                Comments

                Comment on this article