3 Search Results for "Lyon, Tim"

Document
DOI: 10.4230/LIPIcs.ICDT.2023.18
Finite-Cliquewidth Sets of Existential Rules: Toward a General Criterion for Decidable yet Highly Expressive Querying

Authors: Thomas Feller, Tim S. Lyon, Piotr Ostropolski-Nalewaja, and Sebastian Rudolph

Published in: LIPIcs, Volume 255, 26th International Conference on Database Theory (ICDT 2023)

Abstract
In our pursuit of generic criteria for decidable ontology-based querying, we introduce finite-cliquewidth sets (fcs) of existential rules, a model-theoretically defined class of rule sets, inspired by the cliquewidth measure from graph theory. By a generic argument, we show that fcs ensures decidability of entailment for a sizable class of queries (dubbed DaMSOQs) subsuming conjunctive queries (CQs). The fcs class properly generalizes the class of finite-expansion sets (fes), and for signatures of arity ≤ 2, the class of bounded-treewidth sets (bts). For higher arities, bts is only indirectly subsumed by fcs by means of reification. Despite the generality of fcs, we provide a rule set with decidable CQ entailment (by virtue of first-order-rewritability) that falls outside fcs, thus demonstrating the incomparability of fcs and the class of finite-unification sets (fus). In spite of this, we show that if we restrict ourselves to single-headed rule sets over signatures of arity ≤ 2, then fcs subsumes fus.
Cite as

Thomas Feller, Tim S. Lyon, Piotr Ostropolski-Nalewaja, and Sebastian Rudolph. Finite-Cliquewidth Sets of Existential Rules: Toward a General Criterion for Decidable yet Highly Expressive Querying. In 26th International Conference on Database Theory (ICDT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 255, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{feller_et_al:LIPIcs.ICDT.2023.18,
  author =	{Feller, Thomas and Lyon, Tim S. and Ostropolski-Nalewaja, Piotr and Rudolph, Sebastian},
  title =	{{Finite-Cliquewidth Sets of Existential Rules: Toward a General Criterion for Decidable yet Highly Expressive Querying}},
  booktitle =	{26th International Conference on Database Theory (ICDT 2023)},
  pages =	{18:1--18:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-270-9},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{255},
  editor =	{Geerts, Floris and Vandevoort, Brecht},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2023.18},
  URN =		{urn:nbn:de:0030-drops-177602},
  doi =		{10.4230/LIPIcs.ICDT.2023.18},
  annote =	{Keywords: existential rules, TGDs, cliquewidth, treewidth, bounded-treewidth sets, finite-unification sets, first-order rewritability, monadic second-order logic, datalog}
}
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-dev.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.CSL.2020.28
Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents

Authors: Tim Lyon, Alwen Tiu, Rajeev Goré, and Ranald Clouston

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
We provide a direct method for proving Craig interpolation for a range of modal and intuitionistic logics, including those containing a "converse" modality. We demonstrate this method for classical tense logic, its extensions with path axioms, and for bi-intuitionistic logic. These logics do not have straightforward formalisations in the traditional Gentzen-style sequent calculus, but have all been shown to have cut-free nested sequent calculi. The proof of the interpolation theorem uses these calculi and is purely syntactic, without resorting to embeddings, semantic arguments, or interpreted connectives external to the underlying logical language. A novel feature of our proof includes an orthogonality condition for defining duality between interpolants.
Cite as

Tim Lyon, Alwen Tiu, Rajeev Goré, and Ranald Clouston. Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 28:1-28:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{lyon_et_al:LIPIcs.CSL.2020.28,
  author =	{Lyon, Tim and Tiu, Alwen and Gor\'{e}, Rajeev and Clouston, Ranald},
  title =	{{Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{28:1--28:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.28},
  URN =		{urn:nbn:de:0030-drops-116713},
  doi =		{10.4230/LIPIcs.CSL.2020.28},
  annote =	{Keywords: Bi-intuitionistic logic, Interpolation, Nested calculi, Proof theory, Sequents, Tense logics}
}
  • Refine by Author
  • 1 Bednarczyk, Bartosz
  • 1 Clouston, Ranald
  • 1 Feller, Thomas
  • 1 Goré, Rajeev
  • 1 Jaakkola, Reijo
  • Show More...

  • Refine by Classification
  • 1 Mathematics of computing → Graph theory
  • 1 Theory of computation → Automated reasoning
  • 1 Theory of computation → Database query languages (principles)
  • 1 Theory of computation → Description logics
  • 1 Theory of computation → Finite Model Theory
  • Show More...

  • Refine by Keyword
  • 1 Bi-intuitionistic logic
  • 1 Craig Interpolation Property
  • 1 Interpolation
  • 1 Nested calculi
  • 1 Proof theory
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2020
  • 1 2022
  • 1 2023

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