Search Results

Documents authored by Bednarczyk, Bartosz

Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.111
On the Limits of Decision: the Adjacent Fragment of First-Order Logic

Authors: Bartosz Bednarczyk, Daumantas Kojelis, and Ian Pratt-Hartmann

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

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.
Cite as

Bartosz Bednarczyk, Daumantas Kojelis, and Ian Pratt-Hartmann. On the Limits of Decision: the Adjacent Fragment of First-Order Logic. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 111:1-111:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bednarczyk_et_al:LIPIcs.ICALP.2023.111,
  author =	{Bednarczyk, Bartosz and Kojelis, Daumantas and Pratt-Hartmann, Ian},
  title =	{{On the Limits of Decision: the Adjacent Fragment of First-Order Logic}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{111:1--111:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.111},
  URN =		{urn:nbn:de:0030-drops-181632},
  doi =		{10.4230/LIPIcs.ICALP.2023.111},
  annote =	{Keywords: decidability, satisfiability, variable-ordered logics, complexity}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2022.15
Towards a Model Theory of Ordered Logics: Expressivity and Interpolation

Authors: Bartosz Bednarczyk and Reijo Jaakkola

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
We consider the family of guarded and unguarded ordered logics, that constitute a recently rediscovered family of decidable fragments of first-order logic (FO), in which the order of quantification of variables coincides with the order in which those variables appear as arguments of predicates. While the complexities of their satisfiability problems are now well-established, their model theory, however, is poorly understood. Our paper aims to provide some insight into it. We start by providing suitable notions of bisimulation for ordered logics. We next employ bisimulations to compare the relative expressive power of ordered logics, and to characterise our logics as bisimulation-invariant fragments of FO à la van Benthem. Afterwards, we study the Craig Interpolation Property (CIP). We refute yet another claim from the infamous work by Purdy, by showing that the fluted and forward fragments do not enjoy CIP. We complement this result by showing that the ordered fragment and the guarded ordered logics enjoy CIP. These positive results rely on novel and quite intricate model constructions, which take full advantage of the "forwardness" of our logics.
Cite as

Bartosz Bednarczyk and Reijo Jaakkola. Towards a Model Theory of Ordered Logics: Expressivity and Interpolation. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 15:1-15:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bednarczyk_et_al:LIPIcs.MFCS.2022.15,
  author =	{Bednarczyk, Bartosz and Jaakkola, Reijo},
  title =	{{Towards a Model Theory of Ordered Logics: Expressivity and Interpolation}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{15:1--15:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.15},
  URN =		{urn:nbn:de:0030-drops-168132},
  doi =		{10.4230/LIPIcs.MFCS.2022.15},
  annote =	{Keywords: ordered fragments, fluted fragment, guarded fragment, model theory, Craig Interpolation Property, expressive power, model checking}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2021.36
On Classical Decidable Logics Extended with Percentage Quantifiers and Arithmetics

Authors: Bartosz Bednarczyk, Maja Orłowska, Anna Pacanowska, and Tony Tan

Published in: LIPIcs, Volume 213, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)

Abstract
During the last decades, a lot of effort was put into identifying decidable fragments of first-order logic. Such efforts gave birth, among the others, to the two-variable fragment and the guarded fragment, depending on the type of restriction imposed on formulae from the language. Despite the success of the mentioned logics in areas like formal verification and knowledge representation, such first-order fragments are too weak to express even the simplest statistical constraints, required for modelling of influence networks or in statistical reasoning. In this work we investigate the extensions of these classical decidable logics with percentage quantifiers, specifying how frequently a formula is satisfied in the indented model. We show, surprisingly, that all the mentioned decidable fragments become undecidable under such extension, sharpening the existing results in the literature. Our negative results are supplemented by decidability of the two-variable guarded fragment with even more expressive counting, namely Presburger constraints. Our results can be applied to infer decidability of various modal and description logics, e.g. Presburger Modal Logics with Converse or ALCI, with expressive cardinality constraints.
Cite as

Bartosz Bednarczyk, Maja Orłowska, Anna Pacanowska, and Tony Tan. On Classical Decidable Logics Extended with Percentage Quantifiers and Arithmetics. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 36:1-36:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bednarczyk_et_al:LIPIcs.FSTTCS.2021.36,
  author =	{Bednarczyk, Bartosz and Or{\l}owska, Maja and Pacanowska, Anna and Tan, Tony},
  title =	{{On Classical Decidable Logics Extended with Percentage Quantifiers and Arithmetics}},
  booktitle =	{41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)},
  pages =	{36:1--36:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-215-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{213},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Chekuri, Chandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2021.36},
  URN =		{urn:nbn:de:0030-drops-155478},
  doi =		{10.4230/LIPIcs.FSTTCS.2021.36},
  annote =	{Keywords: statistical reasoning, knowledge representation, satisfiability, fragments of first-order logic, guarded fragment, two-variable fragment, (un)decidability}
}
Document
DOI: 10.4230/LIPIcs.TIME.2020.17
A Note on C² Interpreted over Finite Data-Words

Authors: Bartosz Bednarczyk and Piotr Witkowski

Published in: LIPIcs, Volume 178, 27th International Symposium on Temporal Representation and Reasoning (TIME 2020)

Abstract
We consider the satisfiability problem for the two-variable fragment of first-order logic extended with counting quantifiers, interpreted over finite words with data, denoted here with C²[≤ , succ, ∼, π_bin]. In our scenario, we allow for using arbitrary many uninterpreted binary predicates from π_bin, two navigational predicates ≤ and succ over word positions as well as a data-equality predicate ∼. We prove that the obtained logic is undecidable, which contrasts with the decidability of the logic without counting by Montanari, Pazzaglia and Sala [Angelo Montanari et al., 2016]. We supplement our results with decidability for several sub-fragments of C²[≤ , succ, ∼, π_bin], e.g. without binary predicates, without successor succ, or under the assumption that the total number of positions carrying the same data value in a data-word is bounded by an a priori given constant.
Cite as

Bartosz Bednarczyk and Piotr Witkowski. A Note on C² Interpreted over Finite Data-Words. In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 17:1-17:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{bednarczyk_et_al:LIPIcs.TIME.2020.17,
  author =	{Bednarczyk, Bartosz and Witkowski, Piotr},
  title =	{{A Note on C² Interpreted over Finite Data-Words}},
  booktitle =	{27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
  pages =	{17:1--17:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-167-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{178},
  editor =	{Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.17},
  URN =		{urn:nbn:de:0030-drops-129850},
  doi =		{10.4230/LIPIcs.TIME.2020.17},
  annote =	{Keywords: Two-variable logic, data-words, VASS, decidability, undecidability, counting}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2017.12
Modulo Counting on Words and Trees

Authors: Bartosz Bednarczyk and Witold Charatonik

Published in: LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)

Abstract
We consider the satisfiability problem for the two-variable fragment of the first-order logic extended with modulo counting quantifiers and interpreted over finite words or trees. We prove a small-model property of this logic, which gives a technique for deciding the satisfiability problem. In the case of words this gives a new proof of EXPSPACE upper bound, and in the case of trees it gives a 2EXPTIME algorithm. This algorithm is optimal: we prove a matching lower bound by a generic reduction from alternating Turing machines working in exponential space; the reduction involves a development of a new version of tiling games.
Cite as

Bartosz Bednarczyk and Witold Charatonik. Modulo Counting on Words and Trees. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bednarczyk_et_al:LIPIcs.FSTTCS.2017.12,
  author =	{Bednarczyk, Bartosz and Charatonik, Witold},
  title =	{{Modulo Counting on Words and Trees}},
  booktitle =	{37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)},
  pages =	{12:1--12:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-055-2},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{93},
  editor =	{Lokam, Satya and Ramanujam, R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.12},
  URN =		{urn:nbn:de:0030-drops-84083},
  doi =		{10.4230/LIPIcs.FSTTCS.2017.12},
  annote =	{Keywords: satisfiability, trees, words, two-variable logic, modulo quantifiers}
}
Document
DOI: 10.4230/LIPIcs.CSL.2017.11
Extending Two-Variable Logic on Trees

Authors: Bartosz Bednarczyk, Witold Charatonik, and Emanuel Kieronski

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract
The finite satisfiability problem for the two-variable fragment of first-order logic interpreted over trees was recently shown to be ExpSpace-complete. We consider two extensions of this logic. We show that adding either additional binary symbols or counting quantifiers to the logic does not affect the complexity of the finite satisfiability problem. However, combining the two extensions and adding both binary symbols and counting quantifiers leads to an explosion of this complexity. We also compare the expressive power of the two-variable fragment over trees with its extension with counting quantifiers. It turns out that the two logics are equally expressive, although counting quantifiers do add expressive power in the restricted case of unordered trees.
Cite as

Bartosz Bednarczyk, Witold Charatonik, and Emanuel Kieronski. Extending Two-Variable Logic on Trees. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bednarczyk_et_al:LIPIcs.CSL.2017.11,
  author =	{Bednarczyk, Bartosz and Charatonik, Witold and Kieronski, Emanuel},
  title =	{{Extending Two-Variable Logic on Trees}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{11:1--11:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.11},
  URN =		{urn:nbn:de:0030-drops-76794},
  doi =		{10.4230/LIPIcs.CSL.2017.11},
  annote =	{Keywords: two-variable logic, trees, satisfiability, expressivity, counting quantifiers}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact