Technischer Bericht TR-2013-07

Bibliograph.
Daten
Kufleitner, Manfred; Lauser, Alexander: Nesting Negations in FO^2 over Finite Words.
Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik, Technischer Bericht Informatik Nr. 2013/07.
19 Seiten, englisch.
CR-Klassif.F.4.1 (Mathematical Logic)
F.4.3 (Formal Languages)
Keywordsregular language; finite monoid; positive variety; first-order logic
Kurzfassung

We consider the fragment Sigma^2_m of two-variable first-order logic FO^2[<] over finite words which is defined by restricting the nesting depth of negations to at most m. Our first result is a combinatorial characterization of Sigma^2_m in terms of so-called rankers. This generalizes a result by Weis and Immerman which we recover as an immediate consequence.

Our second result is an effective algebraic characterization of Sigma^2_m, i.e., for every integer m one can decide whether a given regular language is definable by a two-variable first-order formula with negation nesting depth at most m. More precisely, for every m we give omega-terms U_m and V_m such that an FO^2-definable language is in Sigma^2_m if and only if its ordered syntactic monoid satisfies the identity U_m \leq V_m.

Volltext und
andere Links
PDF (611034 Bytes)
Kontaktkufleitner@fmi.uni-stuttgart.de
Abteilung(en)Universität Stuttgart, Institut für Formale Methoden der Informatik, Theoretische Informatik
Eingabedatum19. September 2013
   Publ. Informatik