Publications

2000

• E. Rosen and J. Tyszkiewicz. SO(∀∃*) sentences and their asymptotic probabilities. Mathematical Logic Quarterly, vol. 46, pp. 435–52, 2000.                                 
  Abstract   BibTeX

  We prove a 0-1 law for the fragment of second order logic SO(AE*) over parametric classes of structures which allow only one unary atomic type, confirming partially a conjecture of Lacoste. This completes the investigation of 0-1 laws for fragments of second order logic (with equality) defined in terms of first order quantifier prefixes over, e.g., simple graphs and tournaments. We also prove a low oscillation law, and establish the 0-1 law for $\Sigma\_1^4(\forall\exists^*)$ without any restriction on the number of unary types.

  @article{RoTy00,
       author = {Eric Rosen and Jurek Tyszkiewicz},
       journal = {Mathematical Logic Quarterly},
       pages = {435--52},
       title = {{{SO}$(\forall\exists^*)$ sentences and their asymptotic probabilities}},
       url = {http://www.logic.rwth-aachen.de/pub/rosen/ae.ps},
       volume = {46},
       year = {2000},
  }
  

1999

• E. Grädel, M. Otto, and E. Rosen. Undecidability Results on Two-Variable Logics. Archive for Mathematical Logic, vol. 38, pp. 213–354, 1999.                                 
  Abstract   BibTeX

  It is a classical result of Mortimer's that L$^2$, first-order logic with two variables, is decidable for satisfiability. It is shown that going beyond L$^2$ by adding any one of the following leads to an undecidable logic:

  – very weak forms of recursion, viz. transitive closure operations, or (restricted) monadic fixed-point operations

  – weak access to cardinalities, through the Härtig (or equicardinality) quantifier, or

  – a choice construct known as Hilbert's epsilon operator.

  In fact all these extensions of L$^2$ prove to be undecidable both for satisfiability, and for satisfiability in finite models. Moreover most of them are hard for $\Sigma\_1^1$, the first level of the analytical hierachy, and thus have a much higher degree of undecidability than first-order logic.

  @article{GraedelOttoRosen98,
       author = {Erich Gr{\"a}del and Martin Otto and Eric Rosen},
       journal = {Archive for Mathematical Logic},
       note = {See also: conference version \cite{GraedelOttoRosen97a}},
       pages = {213--354},
       title = {{Undecidability Results on Two-Variable Logics}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/gor.ps},
       volume = {38},
       year = {1999},
  }
  

• E. Grädel and E. Rosen. Preservation theorems for two-variable logic. Mathematical Logic Quarterly, vol. 45, pp. 315–325, 1999.                                 
  Abstract   BibTeX

  We show that the existential preservation theorem fails for FO$^2$, two-variable first-order logic. It is known that for all k > 2, FO$^k$ does not have an existential preservation theorem, so this settles the last open case, answering a question of Andreka, van Benthem, and Nemeti. In contrast, we prove that the homomorphism preservation theorem holds for FO$^2$.

  @article{GrRo99,
       author = {Erich Gr{\"a}del and Eric Rosen},
       journal = {Mathematical Logic Quarterly},
       pages = {315--325},
       title = {{Preservation theorems for two-variable logic}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/preservation.ps},
       volume = {45},
       year = {1999},
  }
  

• E. Grädel and E. Rosen. Two-variable descriptions of regularity. In Proceedings of 14th IEEE Symposium on Logic in Computer Science LICS `99, Trento, pp. 14–23, 1999.             
  BibTeX

  @inproceedings{GrRo99b,
       author = {Erich Gr{\"a}del and Eric Rosen},
       booktitle = {{Proceedings of 14th IEEE Symposium on Logic in Computer Science LICS `99, Trento}},
       pages = {14--23},
       title = {{Two-variable descriptions of regularity}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/GrRo-lics99.ps},
       year = {1999},
  }
  

• E. Rosen. An existential fragment of second order logic. Archive for Mathematical Logic, vol. 38, pp. 217–234, 1999.                                 
  Abstract   BibTeX

  In this paper, we examine an existential fragment of second order logic, SO(E), which consists of all those second order sentences in which all first order quantifiers are existential. In particular, we are interested in analyzing the expressive power of this logic over the class of finite structures. First, we establish the decidability of its satisfaction problem, using a theorem due to Nesetril and Rodl. We then prove some facts about the expressive power of SO(E) over finite structures. In particular, we show how the Nesetril and Rodl theorem can be used to obtain non-definability results. We also consider the finite variable fragments of SO(E), and use the same machinery to prove that they form a strict hierarchy. Finally, it is shown that for every purely relational finite model \textbfA whose signature contains a relation symbol of arity > 3, the property of containing a submodel isomorphic to \textbfA is not expressible by any SO(E) sentence containing less than |\textbfA| ( reusable) first order variables.

  @article{Ro99,
       author = {Eric Rosen},
       journal = {Archive for Mathematical Logic},
       pages = {217--234},
       title = {{An existential fragment of second order logic}},
       url = {http://www.logic.rwth-aachen.de/pub/rosen/archiv.ps},
       volume = {38},
       year = {1999},
  }
  

1998

• E. Rosen. On the first-order prefix hierarchy. 1998.                                 
  Abstract   BibTeX

  We investigate the expressive power of fragments of first-order logic that are defined in terms of prefixes. The main result establishes a strict hierarchy among those fragments over the signature of a single binary relation. It implies that for each prefix $p$, there is a sentence $\phi\_p$ in prefix normal form with prefix $p$, over a single binary relation, such that for all sentences $\theta$ in prenex normal form, of $\theta$ is equivalent to $\phi\_p$, then $p$ can be embedded in the prefix of $\theta$. This strengthens a theorem of Walkoe.

  @misc{Rosen98,
       annote = {Preprint},
       author = {Eric Rosen},
       title = {{On the first-order prefix hierarchy}},
       url = {http://www.logic.rwth-aachen.de/pub/rosen/Rosen98.ps},
       year = {1998},
  }
  

1997

• E. Grädel, M. Otto, and E. Rosen. Two-Variable Logic with Counting is Decidable. In Proceedings of 12th IEEE Symposium on Logic in Computer Science LICS `97, Warschau, 1997.                                 
  Abstract   BibTeX

  The satisfiability problem for C2 is shown to be decidable. \par C$^2$ is first-order logic with only two variables in the presence of arbitrary counting quantifiers of the form ''there exist at least m''. It considerably extends L$^2$, plain first-order with only two variables, which is known to be decidable by a result of Mortimer. Unlike L$^2$, C$^2$ does not have the finite model property. As C$^2$ extends L$^2$ by expressive means for counting, significant applications arise from the fact that C$^2$ embeds corresponding counting extensions of modal logics.

  @inproceedings{GraedelOttoRosen97,
       author = {Erich Gr{\"a}del and Martin Otto and Eric Rosen},
       booktitle = {{Proceedings of 12th IEEE Symposium on Logic in Computer Science LICS `97, Warschau}},
       title = {{Two-Variable Logic with Counting is Decidable}},
       url = {http://www.logic.rwth-aachen.de/pub/graedel/gorc2.ps},
       year = {1997},
  }
  

• E. Grädel, M. Otto, and E. Rosen. Undecidability Results on Two-Variable Logics. In Proceedings of 14th Symposium on Theoretical Aspects of Computer Science STACS`97, vol. 1200 of Lecture Notes in Computer Science, pp. 249–260, 1997.             
  BibTeX

  @inproceedings{GraedelOttoRosen97a,
       author = {Erich Gr{\"a}del and Martin Otto and Eric Rosen},
       booktitle = {{Proceedings of 14th Symposium on Theoretical Aspects of Computer Science STACS`97}},
       note = {See also: journal version \cite{GraedelOttoRosen98}},
       pages = {249--260},
       series = {{Lecture Notes in Computer Science}},
       title = {{Undecidability Results on Two-Variable Logics}},
       volume = {1200},
       year = {1997},
  }
  

• E. Rosen. Modal logic over finite structures. Journal of Logic, Language and Information, vol. 6, pp. 427–439, 1997.                                 
  Abstract   BibTeX

  We investigate properties of propositional modal logic over the class of finite structures. In particular, we show that certain known preservation theorems remain true over this class. We prove that a class of finite models is defined by a first-order sentence and closed under bisimulations if and only if it is definable by a modal formula. We also prove that a class of finite models defined by a modal formula is closed under extensions if and only if it is defined by a \verb $\Diamond$-modal formula.

  @article{Ro97,
       author = {Eric Rosen},
       journal = {Journal of Logic, Language and Information},
       pages = {427--439},
       title = {{Modal logic over finite structures}},
       url = {http://www.logic.rwth-aachen.de/pub/rosen/jolli.ps},
       volume = {6},
       year = {1997},
  }