22 Search Results for "Grädel, Erich"


Document
Ehrenfeucht-Fraïssé Games in Semiring Semantics

Authors: Sophie Brinke, Erich Grädel, and Lovro Mrkonjić

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)


Abstract
Ehrenfeucht-Fraïssé games provide a fundamental method for proving elementary equivalence (and equivalence up to a certain quantifier rank) of relational structures. We investigate the soundness and completeness of this method in the more general context of semiring semantics. Motivated originally by provenance analysis of database queries, semiring semantics evaluates logical statements not just by true or false, but by values in some commutative semiring; this can provide much more detailed information, for instance concerning the combinations of atomic facts that imply the truth of a statement, or practical information about evaluation costs, confidence scores, access levels or the number of successful evaluation strategies. There is a wide variety of different semirings that are relevant for provenance analysis, and the applicability of classical logical methods in semiring semantics may strongly depend on the algebraic properties of the underlying semiring. While Ehrenfeucht-Fraïssé games are sound and complete for logical equivalences in classical semantics, and thus on the Boolean semiring, this is in general not the case for other semirings. We provide a detailed analysis of the soundness and completeness of model comparison games on specific semirings, not just for classical Ehrenfeucht-Fraïssé games but also for other variants based on bijections or counting. Finally we propose a new kind of games, called homomorphism games, based on the fact that there exist locally very different semiring interpretations that can be proved to be elementarily equivalent via separating sets of homomorphisms. We prove that these homomorphism games provide a sound and complete method for logical equivalences on finite lattice semirings.

Cite as

Sophie Brinke, Erich Grädel, and Lovro Mrkonjić. Ehrenfeucht-Fraïssé Games in Semiring Semantics. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 19:1-19:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{brinke_et_al:LIPIcs.CSL.2024.19,
  author =	{Brinke, Sophie and Gr\"{a}del, Erich and Mrkonji\'{c}, Lovro},
  title =	{{Ehrenfeucht-Fra\"{i}ss\'{e} Games in Semiring Semantics}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{19:1--19:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello 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.CSL.2024.19},
  URN =		{urn:nbn:de:0030-drops-196623},
  doi =		{10.4230/LIPIcs.CSL.2024.19},
  annote =	{Keywords: Semiring semantics, elementary equivalence, Ehrenfeucht-Fra\"{i}ss\'{e} games}
}
Document
Locality Theorems in Semiring Semantics

Authors: Clotilde Bizière, Erich Grädel, and Matthias Naaf

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)


Abstract
Semiring semantics of first-order logic generalises classical Boolean semantics by permitting truth values from a commutative semiring, which can model information such as costs or access restrictions. This raises the question to what extent classical model-theoretic properties still apply, and how this depends on the algebraic properties of the semiring. In this paper, we study this question for the classical locality theorems due to Hanf and Gaifman. We prove that Hanf’s locality theorem generalises to all semirings with idempotent operations, but fails for many non-idempotent semirings. We then consider Gaifman normal forms and show that for formulae with free variables, Gaifman’s theorem does not generalise beyond the Boolean semiring. Also for sentences, it fails in the natural semiring and the tropical semiring. Our main result, however, is a constructive proof of the existence of Gaifman normal forms for min-max and lattice semirings. The proof implies a stronger version of Gaifman’s classical theorem in Boolean semantics: every sentence has a Gaifman normal form which does not add negations.

Cite as

Clotilde Bizière, Erich Grädel, and Matthias Naaf. Locality Theorems in Semiring Semantics. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 20:1-20:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{biziere_et_al:LIPIcs.MFCS.2023.20,
  author =	{Bizi\`{e}re, Clotilde and Gr\"{a}del, Erich and Naaf, Matthias},
  title =	{{Locality Theorems in Semiring Semantics}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{20:1--20:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.20},
  URN =		{urn:nbn:de:0030-drops-185546},
  doi =		{10.4230/LIPIcs.MFCS.2023.20},
  annote =	{Keywords: Semiring semantics, Locality, First-order logic}
}
Document
Logic and Random Discrete Structures (Dagstuhl Seminar 22061)

Authors: Erich Grädel, Phokion G. Kolaitis, Marc Noy, and Matthias Naaf

Published in: Dagstuhl Reports, Volume 12, Issue 2 (2022)


Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 22061 "Logic and Random Discrete Structures". The main topic of this seminar has been the analysis of large random discrete structures, such as trees, graphs, or permutations, from the perspective of mathematical logic. It has brought together both experts and junior researchers from a number of different areas where logic and random structures play a role, with the goal to establish new connections between such areas and to encourage interactions between foundational research and different application areas, including probabilistic databases.

Cite as

Erich Grädel, Phokion G. Kolaitis, Marc Noy, and Matthias Naaf. Logic and Random Discrete Structures (Dagstuhl Seminar 22061). In Dagstuhl Reports, Volume 12, Issue 2, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@Article{gradel_et_al:DagRep.12.2.1,
  author =	{Gr\"{a}del, Erich and Kolaitis, Phokion G. and Noy, Marc and Naaf, Matthias},
  title =	{{Logic and Random Discrete Structures (Dagstuhl Seminar 22061)}},
  pages =	{1--16},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2022},
  volume =	{12},
  number =	{2},
  editor =	{Gr\"{a}del, Erich and Kolaitis, Phokion G. and Noy, Marc and Naaf, Matthias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.12.2.1},
  URN =		{urn:nbn:de:0030-drops-169295},
  doi =		{10.4230/DagRep.12.2.1},
  annote =	{Keywords: combinatorics, complexity theory, logic, random structures, probabilistic databases}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
Elementary Equivalence Versus Isomorphism in Semiring Semantics

Authors: Erich Grädel and Lovro Mrkonjić

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)


Abstract
We study the first-order axiomatisability of finite semiring interpretations or, equivalently, the question whether elementary equivalence and isomorphism coincide for valuations of atomic facts over a finite universe into a commutative semiring. Contrary to the classical case of Boolean semantics, where every finite structure is axiomatised up to isomorphism by a first-order sentence, the situation in semiring semantics is rather different, and depends on the underlying semiring. We prove that for a number of important semirings, including min-max semirings, and the semirings of positive Boolean expressions, there exist finite semiring interpretations that are elementarily equivalent but not isomorphic. The same is true for the polynomial semirings that are universal for the classes of absorptive, idempotent, and fully idempotent semirings, respectively. On the other side, we prove that for other, practically relevant, semirings such as the Viterby semiring 𝕍, the tropical semiring 𝕋, the natural semiring ℕ and the universal polynomial semiring ℕ[X], all finite semiring interpretations are first-order axiomatisable, and thus elementary equivalence implies isomorphism.

Cite as

Erich Grädel and Lovro Mrkonjić. Elementary Equivalence Versus Isomorphism in Semiring Semantics. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 133:1-133:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{gradel_et_al:LIPIcs.ICALP.2021.133,
  author =	{Gr\"{a}del, Erich and Mrkonji\'{c}, Lovro},
  title =	{{Elementary Equivalence Versus Isomorphism in Semiring Semantics}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{133:1--133:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.133},
  URN =		{urn:nbn:de:0030-drops-142022},
  doi =		{10.4230/LIPIcs.ICALP.2021.133},
  annote =	{Keywords: Semiring semantics, elementary equivalence, axiomatisability}
}
Document
Semiring Provenance for Fixed-Point Logic

Authors: Katrin M. Dannert, Erich Grädel, Matthias Naaf, and Val Tannen

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)


Abstract
Semiring provenance is a successful approach, originating in database theory, to providing detailed information on how atomic facts combine to yield the result of a query. In particular, general provenance semirings of polynomials or formal power series provide precise descriptions of the evaluation strategies or "proof trees" for the query. By evaluating these descriptions in specific application semirings, one can extract practical information for instance about the confidence of a query or the cost of its evaluation. This paper develops semiring provenance for very general logical languages featuring the full interaction between negation and fixed-point inductions or, equivalently, arbitrary interleavings of least and greatest fixed points. This also opens the door to provenance analysis applications for modal μ-calculus and temporal logics, as well as for finite and infinite model-checking games. Interestingly, the common approach based on Kleene’s Fixed-Point Theorem for ω-continuous semirings is not sufficient for these general languages. We show that an adequate framework for the provenance analysis of full fixed-point logics is provided by semirings that are (1) fully continuous, and (2) absorptive. Full continuity guarantees that provenance values of least and greatest fixed-points are well-defined. Absorptive semirings provide a symmetry between least and greatest fixed-points and make sure that provenance values of greatest fixed points are informative. We identify semirings of generalized absorptive polynomials S^{∞}[X] and prove universal properties that make them the most general appropriate semirings for our framework. These semirings have the further property of being (3) chain-positive, which is responsible for having truth-preserving interpretations that give non-zero values to all true formulae. We relate the provenance analysis of fixed-point formulae with provenance values of plays and strategies in the associated model-checking games. Specifically, we prove that the provenance value of a fixed point formula gives precise information on the evaluation strategies in these games.

Cite as

Katrin M. Dannert, Erich Grädel, Matthias Naaf, and Val Tannen. Semiring Provenance for Fixed-Point Logic. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 17:1-17:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{dannert_et_al:LIPIcs.CSL.2021.17,
  author =	{Dannert, Katrin M. and Gr\"{a}del, Erich and Naaf, Matthias and Tannen, Val},
  title =	{{Semiring Provenance for Fixed-Point Logic}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{17:1--17:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.17},
  URN =		{urn:nbn:de:0030-drops-134518},
  doi =		{10.4230/LIPIcs.CSL.2021.17},
  annote =	{Keywords: Finite Model Theory, Semiring Provenance, Absorptive Semirings, Fixed-Point Logics}
}
Document
Choiceless Computation and Symmetry: Limitations of Definability

Authors: Benedikt Pago

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)


Abstract
The search for a logic capturing PTIME is a long standing open problem in finite model theory. One of the most promising candidate logics for this is Choiceless Polynomial Time with counting (CPT). Abstractly speaking, CPT is an isomorphism-invariant computation model working with hereditarily finite sets as data structures. While it is easy to check that the evaluation of CPT-sentences is possible in polynomial time, the converse has been open for more than 20 years: Can every PTIME-decidable property of finite structures be expressed in CPT? We attempt to make progress towards a negative answer and show that Choiceless Polynomial Time cannot compute a preorder with colour classes of logarithmic size in every hypercube. The reason is that such preorders have super-polynomially many automorphic images, which makes it impossible for CPT to define them. While the computation of such a preorder is not a decision problem that would immediately separate P and CPT, it is significant for the following reason: The so-called Cai-Fürer-Immerman (CFI) problem is one of the standard "benchmarks" for logics and maybe best known for separating fixed-point logic with counting (FPC) from P. Hence, it is natural to consider this also a potential candidate for the separation of CPT and P. The strongest known positive result in this regard says that CPT is able to solve CFI if a preorder with logarithmically sized colour classes is present in the input structure. Our result implies that this approach cannot be generalised to unordered inputs. In other words, CFI on unordered hypercubes is a PTIME-problem which provably cannot be tackled with the state-of-the-art choiceless algorithmic techniques.

Cite as

Benedikt Pago. Choiceless Computation and Symmetry: Limitations of Definability. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 33:1-33:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{pago:LIPIcs.CSL.2021.33,
  author =	{Pago, Benedikt},
  title =	{{Choiceless Computation and Symmetry: Limitations of Definability}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{33:1--33:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.33},
  URN =		{urn:nbn:de:0030-drops-134673},
  doi =		{10.4230/LIPIcs.CSL.2021.33},
  annote =	{Keywords: finite model theory, descriptive complexity, choiceless computation, symmetries of combinatorial objects}
}
Document
Guarded Teams: The Horizontally Guarded Case

Authors: Erich Grädel and Martin Otto

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


Abstract
Team semantics admits reasoning about large sets of data, modelled by sets of assignments (called teams), with first-order syntax. This leads to high expressive power and complexity, particularly in the presence of atomic dependency properties for such data sets. It is therefore interesting to explore fragments and variants of logic with team semantics that permit model-theoretic tools and algorithmic methods to control this explosion in expressive power and complexity. We combine here the study of team semantics with the notion of guarded logics, which are well-understood in the case of classical Tarski semantics, and known to strike a good balance between expressive power and algorithmic manageability. In fact there are two strains of guardedness for teams. Horizontal guardedness requires the individual assignments of the team to be guarded in the usual sense of guarded logics. Vertical guardedness, on the other hand, posits an additional (or definable) hypergraph structure on relational structures in order to interpret a constraint on the component-wise variability of assignments within teams. In this paper we investigate the horizontally guarded case. We study horizontally guarded logics for teams and appropriate notions of guarded team bisimulation. In particular, we establish characterisation theorems that relate invariance under guarded team bisimulation with guarded team logics, but also with logics under classical Tarski semantics.

Cite as

Erich Grädel and Martin Otto. Guarded Teams: The Horizontally Guarded Case. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{gradel_et_al:LIPIcs.CSL.2020.22,
  author =	{Gr\"{a}del, Erich and Otto, Martin},
  title =	{{Guarded Teams: The Horizontally Guarded Case}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{22:1--22:17},
  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.22},
  URN =		{urn:nbn:de:0030-drops-116650},
  doi =		{10.4230/LIPIcs.CSL.2020.22},
  annote =	{Keywords: Team semantics, guarded logics, bisimulation, characterisation theorems}
}
Document
Choiceless Logarithmic Space

Authors: Erich Grädel and Svenja Schalthöfer

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)


Abstract
One of the most important open problems in finite model theory is the question whether there is a logic characterising efficient computation. While this question usually concerns Ptime, it can also be applied to other complexity classes, and in particular to Logspace which can be seen as a formalisation of efficient computation for big data. One of the strongest candidates for a logic capturing Ptime is Choiceless Polynomial Time (CPT). It is based on the idea of choiceless algorithms, a general model of symmetric computation over abstract structures (rather than their encodings by finite strings). However, there is currently neither a comparably strong candidate for a logic for Logspace, nor a logic transferring the idea of choiceless computation to Logspace. We propose here a notion of Choiceless Logarithmic Space which overcomes some of the obstacles posed by Logspace as a less robust complexity class. The resulting logic is contained in both Logspace and CPT, and is strictly more expressive than all logics for Logspace that have been known so far. Further, we address the question whether this logic can define all Logspace-queries, and prove that this is not the case.

Cite as

Erich Grädel and Svenja Schalthöfer. Choiceless Logarithmic Space. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 31:1-31:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{gradel_et_al:LIPIcs.MFCS.2019.31,
  author =	{Gr\"{a}del, Erich and Schalth\"{o}fer, Svenja},
  title =	{{Choiceless Logarithmic Space}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{31:1--31:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.31},
  URN =		{urn:nbn:de:0030-drops-109758},
  doi =		{10.4230/LIPIcs.MFCS.2019.31},
  annote =	{Keywords: Finite Model Theory, Logics for Logspace, Choiceless Computation}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
Approximations of Isomorphism and Logics with Linear-Algebraic Operators (Track B: Automata, Logic, Semantics, and Theory of Programming)

Authors: Anuj Dawar, Erich Grädel, and Wied Pakusa

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)


Abstract
Invertible map equivalences are approximations of graph isomorphism that refine the well-known Weisfeiler-Leman method. They are parameterized by a number k and a set Q of primes. The intuition is that two equivalent graphs G equiv^IM_{k, Q} H cannot be distinguished by means of partitioning the set of k-tuples in both graphs with respect to any linear-algebraic operator acting on vector spaces over fields of characteristic p, for any p in Q. These equivalences have first appeared in the study of rank logic, but in fact they can be used to delimit the expressive power of any extension of fixed-point logic with linear-algebraic operators. We define {LA^{k}}(Q), an infinitary logic with k variables and all linear-algebraic operators over finite vector spaces of characteristic p in Q and show that equiv^IM_{k, Q} is the natural notion of elementary equivalence for this logic. The logic LA^{omega}(Q) = Cup_{k in omega} LA^{k}(Q) is then a natural upper bound on the expressive power of any extension of fixed-point logics by means of Q-linear-algebraic operators. By means of a new and much deeper algebraic analysis of a generalized variant, for any prime p, of the CFI-structures due to Cai, Fürer, and Immerman, we prove that, as long as Q is not the set of all primes, there is no k such that equiv^IM_{k, Q} is the same as isomorphism. It follows that there are polynomial-time properties of graphs which are not definable in LA^{omega}(Q), which implies that no extension of fixed-point logic with linear-algebraic operators can capture PTIME, unless it includes such operators for all prime characteristics. Our analysis requires substantial algebraic machinery, including a homogeneity property of CFI-structures and Maschke’s Theorem, an important result from the representation theory of finite groups.

Cite as

Anuj Dawar, Erich Grädel, and Wied Pakusa. Approximations of Isomorphism and Logics with Linear-Algebraic Operators (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 112:1-112:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{dawar_et_al:LIPIcs.ICALP.2019.112,
  author =	{Dawar, Anuj and Gr\"{a}del, Erich and Pakusa, Wied},
  title =	{{Approximations of Isomorphism and Logics with Linear-Algebraic Operators}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{112:1--112:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.112},
  URN =		{urn:nbn:de:0030-drops-106887},
  doi =		{10.4230/LIPIcs.ICALP.2019.112},
  annote =	{Keywords: Finite Model Theory, Graph Isomorphism, Descriptive Complexity, Algebra}
}
Document
Logics for Dependence and Independence (Dagstuhl Seminar 19031)

Authors: Erich Grädel, Phokion G. Kolaitis, Juha Kontinen, and Heribert Vollmer

Published in: Dagstuhl Reports, Volume 9, Issue 1 (2019)


Abstract
This report documents the programme and outcomes of Dagstuhl Seminar 19031 "Logics for Dependence and Independence". This seminar served as a follow-up seminar to the highly successful seminars "Dependence Logic: Theory and Applications" (13071) and "Logics for Dependence and Independence" (15261). A key objective of the seminar was to bring together researchers working in dependence logic and in the application areas so that they can communicate state-of-the-art advances and embark on a systematic interaction. The goal was especially to reach those researchers who have recently started working in this thriving area as well as researchers working on several aspects of database theory, separation logic, and logics of uncertainy.

Cite as

Erich Grädel, Phokion G. Kolaitis, Juha Kontinen, and Heribert Vollmer. Logics for Dependence and Independence (Dagstuhl Seminar 19031). In Dagstuhl Reports, Volume 9, Issue 1, pp. 28-46, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@Article{gradel_et_al:DagRep.9.1.28,
  author =	{Gr\"{a}del, Erich and Kolaitis, Phokion G. and Kontinen, Juha and Vollmer, Heribert},
  title =	{{Logics for Dependence and Independence (Dagstuhl Seminar 19031)}},
  pages =	{28--46},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2019},
  volume =	{9},
  number =	{1},
  editor =	{Gr\"{a}del, Erich and Kolaitis, Phokion G. and Kontinen, Juha and Vollmer, Heribert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.9.1.28},
  URN =		{urn:nbn:de:0030-drops-105682},
  doi =		{10.4230/DagRep.9.1.28},
  annote =	{Keywords: dependence logic, mathematical logic, computational complexity, finite model theory, game theory}
}
Document
Dependency Concepts up to Equivalence

Authors: Erich Grädel and Matthias Hoelzel

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)


Abstract
Modern logics of dependence and independence are based on different variants of atomic dependency statements (such as dependence, exclusion, inclusion, or independence) and on team semantics: A formula is evaluated not with a single assignment of values to the free variables, but with a set of such assignments, called a team. In this paper we explore logics of dependence and independence where the atomic dependency statements cannot distinguish elements up to equality, but only up to a given equivalence relation (which may model observational indistinguishabilities, for instance between states of a computational process or between values obtained in an experiment). Our main goal is to analyse the power of such logics, by identifying equally expressive fragments of existential second-order logic or greatest fixed-point logic, with relations that are closed under the given equivalence. Using an adaptation of the Ehrenfeucht-Fraïssé method we further study conditions on the given equivalences under which these logics collapse to first-order logic, are equivalent to full existential second-order logic, or are strictly between first-order and existential second-order logic.

Cite as

Erich Grädel and Matthias Hoelzel. Dependency Concepts up to Equivalence. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 25:1-25:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{gradel_et_al:LIPIcs.CSL.2018.25,
  author =	{Gr\"{a}del, Erich and Hoelzel, Matthias},
  title =	{{Dependency Concepts up to Equivalence}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{25:1--25:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.25},
  URN =		{urn:nbn:de:0030-drops-96921},
  doi =		{10.4230/LIPIcs.CSL.2018.25},
  annote =	{Keywords: Logics of dependence and independence, Team semantics, Existential second-order logic, Observational equivalence, Expressive power}
}
Document
Finite and Algorithmic Model Theory (Dagstuhl Seminar 17361)

Authors: Anuj Dawar, Erich Grädel, Phokion G. Kolaitis, and Thomas Schwentick

Published in: Dagstuhl Reports, Volume 7, Issue 9 (2018)


Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 17361 "Finite and Algorithmic Model Theory".

Cite as

Anuj Dawar, Erich Grädel, Phokion G. Kolaitis, and Thomas Schwentick. Finite and Algorithmic Model Theory (Dagstuhl Seminar 17361). In Dagstuhl Reports, Volume 7, Issue 9, pp. 1-25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@Article{dawar_et_al:DagRep.7.9.1,
  author =	{Dawar, Anuj and Gr\"{a}del, Erich and Kolaitis, Phokion G. and Schwentick, Thomas},
  title =	{{Finite and Algorithmic Model Theory (Dagstuhl Seminar 17361)}},
  pages =	{1--25},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2018},
  volume =	{7},
  number =	{9},
  editor =	{Dawar, Anuj and Gr\"{a}del, Erich and Kolaitis, Phokion G. and Schwentick, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.7.9.1},
  URN =		{urn:nbn:de:0030-drops-85863},
  doi =		{10.4230/DagRep.7.9.1},
  annote =	{Keywords: algorithms, database theory, descriptive complexity, finite model theory, independence logic, knowledge representation, model checking}
}
Document
The Model-Theoretic Expressiveness of Propositional Proof Systems

Authors: Erich Grädel, Benedikt Pago, and Wied Pakusa

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


Abstract
We establish new, and surprisingly tight, connections between propositional proof complexity and finite model theory. Specifically, we show that the power of several propositional proof systems, such as Horn resolution, bounded width resolution, and the polynomial calculus of bounded degree, can be characterised in a precise sense by variants of fixed-point logics that are of fundamental importance in descriptive complexity theory. Our main results are that Horn resolution has the same expressive power as least fixed-point logic, that bounded width resolution captures existential least fixed-point logic, and that the (monomial restriction of the) polynomial calculus of bounded degree solves precisely the problems definable in fixed-point logic with counting.

Cite as

Erich Grädel, Benedikt Pago, and Wied Pakusa. The Model-Theoretic Expressiveness of Propositional Proof Systems. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{gradel_et_al:LIPIcs.CSL.2017.27,
  author =	{Gr\"{a}del, Erich and Pago, Benedikt and Pakusa, Wied},
  title =	{{The Model-Theoretic Expressiveness of Propositional Proof Systems}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{27:1--27:18},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.27},
  URN =		{urn:nbn:de:0030-drops-76897},
  doi =		{10.4230/LIPIcs.CSL.2017.27},
  annote =	{Keywords: Propositional proof systems, fixed-point logics, resolution, polynomial calculus, generalized quantifiers}
}
Document
Advice Automatic Structures and Uniformly Automatic Classes

Authors: Faried Abu Zaid, Erich Grädel, and Frederic Reinhardt

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


Abstract
We study structures that are automatic with advice. These are structures that admit a presentation by finite automata (over finite or infinite words or trees) with access to an additional input,called an advice. Over finite words, a standard example of a structure that is automatic with advice, but not automatic in the classical sense, is the additive group of rational numbers (Q,+). By using a set of advices rather than a single advice, this leads to the new concept of a parameterised automatic presentation as a means to uniformly represent a whole class of structures. The decidability of the first-order theory of such a uniformly automatic class reduces to the decidability of the monadic second-order theory of the set of advices that are used in the presentation. Such decidability results also hold for extensions of first-order logic by regularity preserving quantifiers, such as cardinality quantifiers and Ramsey quantifiers. To investigate the power of this concept, we present examples of structures and classes of structures that are automatic with advice but not without advice, and we prove classification theorems for the structures with an advice automatic presentation for several algebraic domains. In particular, we prove that the class of all torsion-free Abelian groups of rank one is uniformly omega-automatic and that there is a uniform omega-tree-automatic presentation of the class of all Abelian groups up to elementary equivalence and of the class of all countable divisible Abelian groups. On the other hand we show that every uniformly omega-automatic class of Abelian groups must have bounded rank. While for certain domains, such as trees and Abelian groups, it turns out that automatic presentations with advice are capable of presenting significantly more complex structures than ordinary automatic presentations, there are other domains, such as Boolean algebras, where this is provably not the case. Further, advice seems to not be of much help for representing some particularly relevant examples of structures with decidable theories, most notably the field of reals. Finally we study closure properties for several kinds of uniformly automatic classes, and decision problems concerning the number of non-isomorphic models in uniformly automatic classes with the unique representation property.

Cite as

Faried Abu Zaid, Erich Grädel, and Frederic Reinhardt. Advice Automatic Structures and Uniformly Automatic Classes. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 35:1-35:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{abuzaid_et_al:LIPIcs.CSL.2017.35,
  author =	{Abu Zaid, Faried and Gr\"{a}del, Erich and Reinhardt, Frederic},
  title =	{{Advice Automatic Structures and Uniformly Automatic Classes}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{35:1--35: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.35},
  URN =		{urn:nbn:de:0030-drops-76971},
  doi =		{10.4230/LIPIcs.CSL.2017.35},
  annote =	{Keywords: automatic structures, algorithmic model theory, decidable theories, torsion-free abelian groups, first-order logic}
}
Document
Counting in Team Semantics

Authors: Erich Grädel and Stefan Hegselmann

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)


Abstract
We explore several counting constructs for logics with team semantics. Counting is an important task in numerous applications, but with a somewhat delicate relationship to logic. Team semantics on the other side is the mathematical basis of modern logics of dependence and independence, in which formulae are evaluated not for a single assignment of values to variables, but for a set of such assignments. It is therefore interesting to ask what kind of counting constructs are adequate in this context, and how such constructs influence the expressive power, and the model-theoretic and algorithmic properties of logics with team semantics. Due to the second-order features of team semantics there is a rich variety of potential counting constructs. Here we study variations of two main ideas: forking atoms and counting quantifiers. Forking counts how many different values for a tuple w occur in assignments with coinciding values for v. We call this the forking degree of bar v with respect to bar w. Forking is powerful enough to capture many of the previously studied atomic dependency properties. In particular we exhibit logics with forking atoms that have, respectively, precisely the power of dependence logic and independence logic. Our second approach uses counting quantifiers E^{geq mu} of a similar kind as used in logics with Tarski semantics. The difference is that these quantifiers are now applied to teams of assignments that may give different values to mu. We show that, on finite structures, there is an intimate connection between inclusion logic with counting quantifiers and FPC, fixed-point logic with counting, which is a logic of fundamental importance for descriptive complexity theory. For sentences, the two logics have the same expressive power. Our analysis is based on a new variant of model-checking games, called threshold safety games, on a trap condition for such games, and on game interpretations.

Cite as

Erich Grädel and Stefan Hegselmann. Counting in Team Semantics. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 35:1-35:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{gradel_et_al:LIPIcs.CSL.2016.35,
  author =	{Gr\"{a}del, Erich and Hegselmann, Stefan},
  title =	{{Counting in Team Semantics}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{35:1--35:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.35},
  URN =		{urn:nbn:de:0030-drops-65757},
  doi =		{10.4230/LIPIcs.CSL.2016.35},
  annote =	{Keywords: logics with counting, team semantics, fixed-point logic with counting}
}
  • Refine by Author
  • 21 Grädel, Erich
  • 4 Pakusa, Wied
  • 3 Dawar, Anuj
  • 3 Kolaitis, Phokion G.
  • 3 Naaf, Matthias
  • Show More...

  • Refine by Classification
  • 8 Theory of computation → Finite Model Theory
  • 2 Theory of computation → Logic
  • 1 Mathematics of computing → Combinatorics
  • 1 Mathematics of computing → Permutations and combinations
  • 1 Theory of computation → Complexity theory and logic

  • Refine by Keyword
  • 4 finite model theory
  • 3 Finite Model Theory
  • 3 Semiring semantics
  • 3 descriptive complexity
  • 3 logic
  • Show More...

  • Refine by Type
  • 22 document

  • Refine by Publication Year
  • 3 2012
  • 3 2019
  • 3 2021
  • 2 2016
  • 2 2017
  • Show More...

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