Otto, Martin (2006)
The boundedness problem for monadic universal first-order logic.
21st Annual IEEE Symposium on Logic in Computer Science (LICS 2006). Seattle, WA (12.08.2006-15.08.2006)
doi: https://doi.ieeecomputersociety.org/10.1109/LICS.2006.50
Konferenzveröffentlichung, Bibliographie
Kurzbeschreibung (Abstract)
We consider the monadic boundedness problem for least fixed points over FO formulae as a decision problem: Given a formula (X, x), positive in X, decide whether there is a uniform finite bound on the least fixed point recursion based on . Few fragments of FO are known to have a decidable boundedness problem; boundedness is known to be undecidable for many fragments. We here show that monadic boundedness is decidable for purely universal FO formulae without equality in which each non-recursive predicate occurs in just one polarity (e.g., only negatively). The restrictions are shown to be essential: waving either the polarity constraint or allowing positive occurrences of equality, the monadic boundedness problem for universal formulae becomes undecidable. The main result is based on a model theoretic analysis involving ideas from modal and guarded logics and...
| Typ des Eintrags: | Konferenzveröffentlichung |
|---|---|
| Erschienen: | 2006 |
| Autor(en): | Otto, Martin |
| Art des Eintrags: | Bibliographie |
| Titel: | The boundedness problem for monadic universal first-order logic |
| Sprache: | Englisch |
| Publikationsjahr: | 2006 |
| Ort: | Los Alamitos, Calif |
| Verlag: | IEEE Computer Society |
| Buchtitel: | 21st Annual IEEE Symposium on Logic in Computer Science |
| Veranstaltungstitel: | 21st Annual IEEE Symposium on Logic in Computer Science (LICS 2006) |
| Veranstaltungsort: | Seattle, WA |
| Veranstaltungsdatum: | 12.08.2006-15.08.2006 |
| DOI: | https://doi.ieeecomputersociety.org/10.1109/LICS.2006.50 |
| Kurzbeschreibung (Abstract): | We consider the monadic boundedness problem for least fixed points over FO formulae as a decision problem: Given a formula (X, x), positive in X, decide whether there is a uniform finite bound on the least fixed point recursion based on . Few fragments of FO are known to have a decidable boundedness problem; boundedness is known to be undecidable for many fragments. We here show that monadic boundedness is decidable for purely universal FO formulae without equality in which each non-recursive predicate occurs in just one polarity (e.g., only negatively). The restrictions are shown to be essential: waving either the polarity constraint or allowing positive occurrences of equality, the monadic boundedness problem for universal formulae becomes undecidable. The main result is based on a model theoretic analysis involving ideas from modal and guarded logics and... |
| Fachbereich(e)/-gebiet(e): | 04 Fachbereich Mathematik |
| Hinterlegungsdatum: | 20 Nov 2008 08:24 |
| Letzte Änderung: | 04 Dez 2024 11:58 |
| PPN: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Frage zum Eintrag |
Optionen (nur für Redakteure)
 |
Redaktionelle Details anzeigen |
Drucken
Impressum