Existential second-order logic over strings
Eiter, Thomas ;
Gottlob, Georg ;
Gurevich, Yuri
Zum Volltext im pdf-Format:
Dokument 1.pdf (484 KB)
Bitte beziehen Sie sich beim Zitieren dieses Dokumentes immer auf folgende
URN: urn:nbn:de:hebis:26-opus-257
URL: http://geb.uni-giessen.de/geb/volltexte/1998/25/
Universität
Justus-Liebig-Universität Gießen
Institut:
Institut für Informatik
Fachgebiet:
Informatik
DDC-Sachgruppe:
Informatik
Dokumentart:
ResearchPaper
Zeitschrift, Serie:
IFIG Research Report
; 9702 / 1997
Sprache:
Englisch
Erstellungsjahr:
1997
Publikationsdatum:
08.07.1998
Kurzfassung auf Englisch:
Existential secondÂorder logic (ESO) and monadic secondÂorder logic (MSO) have attracted much interest in logic and computer science. ESO is a much more expressive logic over word structures than MSO. However, little was known about the relationship between MSO and syntactic fragments of ESO. We shed light on this issue by completely characterizing this relationship for the prefix classes of ESO over strings, (i.e., finite word structures). Moreover, we determine the complexity of model checking over strings, for all ESOÂprefix classes. Let ESO(Q) denote the prefix class containing all sentences of the shape 9RQ' where R is a list of predicate variables, Q is a firstÂorder quantifier prefix from the prefix set Q, and ' is quantifier free. We show that ESO(9 \Lambda 89 \Lambda ) and ESO(9 \Lambda 88) are the maximal standard ESOÂprefix classes contained in MSO, thus expressing only regular languages. We further prove the following dichotomy theorem: An ESO prefixÂclass either expresses only regular languages (and is thus in MSO), or it expresses some NPÂcomplete languages. We also give a precise characterization of those ESOÂprefix classes which are equivalent to MSO over strings, and of the ESOÂprefix classes which are closed under complementation on strings.
Lizenz:
Veröffentlichungsvertrag für Publikationen ohne Print on Demand
