Inproceedings3277: Unterschied zwischen den Versionen

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche
Keine Bearbeitungszusammenfassung
Keine Bearbeitungszusammenfassung
Zeile 2: Zeile 2:
|ErsterAutorVorname=Bartosz
|ErsterAutorVorname=Bartosz
|ErsterAutorNachname=Bednarczyk
|ErsterAutorNachname=Bednarczyk
|FurtherAuthors= Ian Pratt-Hartmann; Daumantas Kojelis
|FurtherAuthors=Ian Pratt-Hartmann; Daumantas Kojelis
}}
}}
{{Inproceedings
{{Inproceedings
Zeile 15: Zeile 15:
}}
}}
{{Publikation Details
{{Publikation Details
|Abstract=We define the adjacent fragment AF of first-order logic, obtained by restricting the sequences of variables occurring as arguments in atomic formulas.
|Abstract=We define the adjacent fragment AF of first-order logic, obtained by restricting the sequences of variables occurring as arguments in atomic formulas. The adjacent fragment generalizes (after a routine renaming) two-variable logic as well as the fluted fragment. We show that the adjacent fragment has the finite model property, and that its satisfiability problem is no harder than for the fluted fragment (and hence is Tower-complete). We further show that any relaxation of the adjacency condition on the allowed order of variables in argument sequences yields a logic whose satisfiability and finite satisfiability problems are undecidable. Finally, we study the effect of the adjacency requirement on the well-known guarded fragment (GF) of first-order logic. We show that the satisfiability problem for the guarded adjacent fragment (GA) remains 2ExpTime-hard, thus strengthening the known lower bound for GF.
The adjacent fragment generalizes (after a routine renaming) two-variable logic as well as the fluted fragment.
We show that the adjacent fragment has the finite model property, and its satisfiability problem is no harder than for the fluted fragment, and hence Tower-complete.
We further show that any relaxation of the adjacency condition on the allowed order of variables in
argument sequences yields a logic whose satisfiability and finite satisfiability problems are undecidable.
Finally, we study the effect of the adjacency requirement on the well-known guarded fragment GF of first-order logic.
We show that the satisfiability problem for the guarded adjacent fragment (GA) remains TwoExpTime-hard,
thus strengthening the known lower bound for GF, but that, in contrast to GF, the fragment GA
has the Craig Interpolation Property.
|Projekt=DeciGUT
|Projekt=DeciGUT
|Forschungsgruppe=Computational Logic
|Forschungsgruppe=Computational Logic
}}
}}

Version vom 4. Mai 2023, 20:42 Uhr

Toggle side column

On the of Limits of Decision: the Adjacent Fragment of First-Order Logic

Bartosz BednarczykBartosz Bednarczyk,  Ian Pratt-HartmannIan Pratt-Hartmann,  Daumantas KojelisDaumantas Kojelis
On the of Limits of Decision: the Adjacent Fragment of First-Order Logic


Bartosz Bednarczyk, Ian Pratt-Hartmann, Daumantas Kojelis
On the of Limits of Decision: the Adjacent Fragment of First-Order Logic
Proceedings of the 50th EATCS International Colloquium on Automata, Languages and Programming, ICALP 2023, Leibniz International Proceedings in Informatics, to appear. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik
  • KurzfassungAbstract
    We define the adjacent fragment AF of first-order logic, obtained by restricting the sequences of variables occurring as arguments in atomic formulas. The adjacent fragment generalizes (after a routine renaming) two-variable logic as well as the fluted fragment. We show that the adjacent fragment has the finite model property, and that its satisfiability problem is no harder than for the fluted fragment (and hence is Tower-complete). We further show that any relaxation of the adjacency condition on the allowed order of variables in argument sequences yields a logic whose satisfiability and finite satisfiability problems are undecidable. Finally, we study the effect of the adjacency requirement on the well-known guarded fragment (GF) of first-order logic. We show that the satisfiability problem for the guarded adjacent fragment (GA) remains 2ExpTime-hard, thus strengthening the known lower bound for GF.
  • Projekt:Project: DeciGUT
  • Forschungsgruppe:Research Group: Computational LogicComputational Logic
@inproceedings{BPK2023,
  author    = {Bartosz Bednarczyk and Ian Pratt-Hartmann and Daumantas Kojelis},
  title     = {On the of Limits of Decision: the Adjacent Fragment of
               First-Order Logic},
  booktitle = {Proceedings of the 50th {EATCS} International Colloquium on
               Automata, Languages and Programming, {ICALP} 2023},
  series    = {Leibniz International Proceedings in Informatics},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  year      = {2023},
  month     = {July}
}