Kieronski, E. ; Otto, Martin (2005)
Small substructures and decidability issues for two-variable first-order logic.
20th IEEE symposium on logic in computer science (LICS 05). Chicago, IL, USA (26.06.2005-29.06.2005)
doi: 10.1109/LICS.2005.49
Konferenzveröffentlichung, Bibliographie
Kurzbeschreibung (Abstract)
We study first-order logic with two variables FO/sup 2/ and establish a small substructure property. Similar to the small model property for FO/sup 2/ we obtain an exponential size bound on embedded substructures, relative to a fixed surrounding structure that may be infinite. We apply this technique to analyse the satisfiability problem for FO/sup 2/ under constraints that require several binary relations to be interpreted as equivalence relations. With a single equivalence relation, FO/sup 2/ has the finite model property and is complete for non-deterministic exponential time, just as for plain FO/sup 2/. With two equivalence relations, FO/sup 2/ does not have the finite model property, but is shown to be decidable via a construction of regular models that admit finite descriptions even though they may necessarily be infinite. For three or more equivalence relations, FO/sup 2/ is undecidable.
| Typ des Eintrags: | Konferenzveröffentlichung |
|---|---|
| Erschienen: | 2005 |
| Autor(en): | Kieronski, E. ; Otto, Martin |
| Art des Eintrags: | Bibliographie |
| Titel: | Small substructures and decidability issues for two-variable first-order logic |
| Sprache: | Englisch |
| Publikationsjahr: | 2005 |
| Ort: | Piscataway |
| Verlag: | IEEE |
| Buchtitel: | 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05) |
| Veranstaltungstitel: | 20th IEEE symposium on logic in computer science (LICS 05) |
| Veranstaltungsort: | Chicago, IL, USA |
| Veranstaltungsdatum: | 26.06.2005-29.06.2005 |
| DOI: | 10.1109/LICS.2005.49 |
| Kurzbeschreibung (Abstract): | We study first-order logic with two variables FO/sup 2/ and establish a small substructure property. Similar to the small model property for FO/sup 2/ we obtain an exponential size bound on embedded substructures, relative to a fixed surrounding structure that may be infinite. We apply this technique to analyse the satisfiability problem for FO/sup 2/ under constraints that require several binary relations to be interpreted as equivalence relations. With a single equivalence relation, FO/sup 2/ has the finite model property and is complete for non-deterministic exponential time, just as for plain FO/sup 2/. With two equivalence relations, FO/sup 2/ does not have the finite model property, but is shown to be decidable via a construction of regular models that admit finite descriptions even though they may necessarily be infinite. For three or more equivalence relations, FO/sup 2/ is undecidable. |
| Fachbereich(e)/-gebiet(e): | 04 Fachbereich Mathematik |
| Hinterlegungsdatum: | 20 Nov 2008 08:21 |
| Letzte Änderung: | 20 Dez 2024 07:37 |
| PPN: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Frage zum Eintrag |
Optionen (nur für Redakteure)
 |
Redaktionelle Details anzeigen |
Drucken
Impressum