pith. sign in

arxiv: 2605.22852 · v1 · pith:FITE5SAZnew · submitted 2026-05-18 · 💻 cs.DB · cs.AI· cs.LG· cs.LO

Expressive Power of Deep Homomorphism Networks over Relational Databases

Moritz Sch\"onherr , Balder ten Cate , Maurice Funk , Benny Kimelfeld , Carsten Lutz , Arie Soeteman This is my paper

Pith reviewed 2026-05-25 00:14 UTC · model grok-4.3

classification 💻 cs.DB cs.AIcs.LGcs.LO
keywords Deep Homomorphism NetworksExpressive PowerUnary Negation FragmentFirst-Order LogicRelational DatabasesSQL QueriesGraph Neural NetworksAggregation Functions
0
0 comments X

The pith

Deep Homomorphism Networks with max, sum and mean aggregations capture exactly the unary negation fragment of first-order logic together with its counting and ratio extensions.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes precise logical characterizations for Deep Homomorphism Networks over relational structures. Networks using max, sum, or mean aggregation correspond to the unary negation fragment of first-order logic and to its extensions by counting quantifiers and ratio quantifiers. Sum-aggregation networks further align with the unary quantifier alternation fragment and with first-order logic augmented by expressive counting. These equivalences also transfer, via the classical first-order-to-SQL correspondence, to statements about the queries that such networks can represent. The characterizations additionally yield decidability results for emptiness and subsumption problems on DHNs, and experiments confirm that the logical distinctions appear in prediction performance.

Core claim

Deep Homomorphism Networks with max, sum, and mean aggregations capture exactly the unary negation fragment of first-order logic along with its extensions by counting quantifiers and ratio quantifiers, while sum-aggregation networks additionally relate to the unary quantifier alternation fragment and to first-order logic with expressive counting; through the FO-SQL correspondence this also characterizes their relation to SQL.

What carries the argument

Deep Homomorphism Networks equipped with max, sum, and mean aggregation functions, which compute via homomorphism-based message passing over relational databases.

If this is right

  • DHNs can represent precisely the queries belonging to UNFO and its listed extensions.
  • Sum-aggregation DHNs can represent queries in the unary quantifier alternation fragment of FO and in FO with expressive counting.
  • Emptiness and subsumption problems for DHNs become decidable via the logical translations.
  • Differences in what queries each aggregation type can express are observable in prediction tasks on relational data.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The results suggest that DHNs are limited to a strict subclass of all first-order queries and therefore cannot express arbitrary SQL without further architectural extensions.
  • The logical equivalences open the possibility of importing static-analysis algorithms from logic directly into DHN model checking.
  • Ratio quantifiers in the logic side may correspond to normalized aggregations that appear in practice but have not yet been studied for DHNs.

Load-bearing premise

The homomorphism network architecture and its aggregation functions are defined such that they directly and exactly capture the semantics of the logical quantifiers in UNFO and its extensions without additional constraints from the neural parameterization or message-passing structure.

What would settle it

A database query that belongs to the unary negation fragment but cannot be realized by any DHN using max, sum, or mean aggregation, or a query realized by such a DHN but outside that fragment, would falsify the claimed equivalence.

Figures

Figures reproduced from arXiv: 2605.22852 by Arie Soeteman, Balder ten Cate, Benny Kimelfeld, Carsten Lutz, Maurice Funk, Moritz Sch\"onherr.

Figure 1
Figure 1. Figure 1: Structure of the databases F m 1 and F m 2 with F m 1 \ F m 2 highlighted in red. Hence, there exists an 1 ≤ i ≤ ℓ such that Ds |= ψi(vs, u¯s). As Duplicator has a winning strategy for the d-round game, it must be the case that (i) h with h(vs) = v3−s and h(u (i) s ) = u (i) 3−s is a homomorphism from Ds|{vs, u (1) s , . . . , u (m) s } to D3−s|{v3−s, u (1) 3−s , . . . , u (n) 3−s }, and (ii) that for any … view at source ↗
Figure 2
Figure 2. Figure 2: The graphs Gn 1 (above) and Gn 2 (below). We omit reflexive and transitive edges. To prove that UQAFO formulas cannot define PQR-orders, we define for each natural number n ∈ N two graphs Gn 1 , Gn 2 : Gn 1 is a PQR-order that contains 3·2 n+1+9 vertices and where the distinguished vertex is the first element in the order. Gn 2 is defined similarly, but it is missing the 2 n + 2-nd vertex that satisfies R.… view at source ↗
Figure 3
Figure 3. Figure 3: In the skeleton graph S u0 each clique vertex ui is connected to a leaf vertex li and each pair of clique vertices ui , uj is connected via a connecting vertex vij . Each connecting vertex is connected to all nodes of a copy of A or B to construct Gu0 or Hu0 . A to vij if ui , uj are in the same triple, and B otherwise. For Hu0 add A to vij if j = i + 1 or i = 0, j = 5, and B otherwise. We show that homomo… view at source ↗
Figure 4
Figure 4. Figure 4: Except from the local transitivity dataset with node classifications [PITH_FULL_IMAGE:figures/full_fig_p054_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Positive example of the sun property E Details on Experiments Both datasets, the code used to generate them, as well as our implementation of DHNs and the experiment code are available in the supplementary material. E.1 Local Transitivity Dataset The local transitivity is a synthetic dataset for vertex classification in a directed graph generated such that the positive examples are locally transitive, and … view at source ↗
Figure 6
Figure 6. Figure 6: Homomorphism queries used in the local transitivity experiment [PITH_FULL_IMAGE:figures/full_fig_p055_6.png] view at source ↗
read the original abstract

The expressive limitations of message-passing Graph Neural Networks (GNNs) have motivated a wide range of more powerful graph learning architectures. We advocate Deep Homomorphism Networks (DHNs) as a model particularly well-suited for learning over relational databases, due to their close connection to important fragments of SQL such as conjunctive queries. We study the precise expressive power of DHNs by relating them to various natural fragments and extensions of first-order logic (FO). For DHNs with max, sum, and mean aggregations, we establish connections to the unary negation fragment (UNFO) and to the extensions of UNFO with counting quantifiers and with ratio quantifiers. We further relate sum-aggregation DHNs to the unary quantifier alternation fragment of FO and to an extension of FO with expressive counting. Through the classical correspondence between FO and SQL, these results also illuminate the relation between DHNs and SQL. They also enable us to study the decidability of two fundamental static analysis problems for DHNs, the emptiness problem and the subsumption problem. Finally, we confirm through experiments that the established differences in expressive power are reflected in the performance on suitable prediction tasks.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 1 minor

Summary. The paper introduces Deep Homomorphism Networks (DHNs) as an architecture well-suited for relational databases due to connections with conjunctive queries. It establishes precise expressive power results by relating DHNs using max, sum, and mean aggregations to the unary negation fragment (UNFO) of first-order logic and its extensions with counting quantifiers and ratio quantifiers. Sum-aggregation DHNs are further connected to the unary quantifier alternation fragment of FO and an extension with expressive counting. Via the FO-SQL correspondence, implications for SQL are discussed. The paper analyzes decidability of the emptiness and subsumption problems for DHNs and provides experiments showing that the theoretical expressive power distinctions appear in prediction task performance.

Significance. If the logical correspondences hold, the work offers a valuable exact characterization of DHN expressive power in terms of well-studied FO fragments, directly enabling decidability results for emptiness and subsumption. This bridges neural architectures with database query languages in a precise way. The experimental confirmation of the distinctions is a positive feature, as is the construction of the model to align with logical semantics via chosen aggregations. The results are significant for guiding architecture design and static analysis in database learning settings.

minor comments (1)
  1. The abstract refers to 'the classical correspondence between FO and SQL' without a specific citation; adding a reference to the relevant theorem would improve traceability for readers.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary of the paper, the assessment of its significance, and the recommendation to accept. No major comments were raised.

Circularity Check

0 steps flagged

No significant circularity; theoretical relations are self-contained

full rationale

The paper establishes expressive power equivalences between DHNs (defined via homomorphism networks and specific aggregations) and fragments of FO/UNFO by direct semantic correspondence. No fitted parameters are renamed as predictions, no self-citations form load-bearing premises, and no ansatz or uniqueness theorem is smuggled in. The derivation chain consists of standard logical translations and SQL-FO correspondences that are external to the paper's definitions. This is the expected non-circular outcome for a theoretical expressivity analysis.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work relies on standard correspondences between first-order logic fragments and SQL without introducing new free parameters, axioms beyond domain-standard logic properties, or invented entities.

axioms (1)
  • domain assumption Known correspondence between first-order logic and SQL
    Invoked to translate logic results into database query implications.

pith-pipeline@v0.9.0 · 5757 in / 1225 out tokens · 29197 ms · 2026-05-25T00:14:18.169242+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

74 extracted references · 74 canonical work pages

  1. [1]

    Bronstein, ˙Ismail ˙Ilkan Ceylan, and Matthias Lanzinger

    Linus Bao, Emily Jin, Michael M. Bronstein, ˙Ismail ˙Ilkan Ceylan, and Matthias Lanzinger. Homomorphism counts as structural encodings for graph learning. InProc. of ICLR. OpenRe- view.net, 2025

    work page 2025

  2. [2]

    Queries with guarded negation.Proc

    Vince Bárány, Balder ten Cate, and Martin Otto. Queries with guarded negation.Proc. VLDB Endow., 5(11):1328–1339, 2012

    work page 2012

  3. [3]

    Graph neural networks with local graph parameters

    Pablo Barceló, Floris Geerts, Juan Reutter, and Maksimilian Ryschkov. Graph neural networks with local graph parameters. InProc. of NeurIPS, pages 25280–25293, 2021

    work page 2021

  4. [4]

    The logical expressiveness of graph neural networks

    Pablo Barceló, Egor V Kostylev, Mikaël Monet, Jorge Pérez, Juan Reutter, and Juan-Pablo Silva. The logical expressiveness of graph neural networks. InProc. of ICLR, April 2020

    work page 2020

  5. [5]

    Decidability of graph neural networks via logical characterizations

    Michael Benedikt, Chia-Hsuan Lu, Boris Motik, and Tony Tan. Decidability of graph neural networks via logical characterizations. InProc. of ICALP, pages 127:1–127:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024

    work page 2024

  6. [6]

    American Mathematical Society Providence, 1966

    Robert Berger.The undecidability of the domino problem. American Mathematical Society Providence, 1966

    work page 1966

  7. [7]

    An overview of query optimization in relational systems

    Surajit Chaudhuri. An overview of query optimization in relational systems. InProc. of PODS, pages 34–43. ACM Press, 1998

    work page 1998

  8. [8]

    Kanatsoulis, and Jure Leskovec

    Tianlang Chen, Charilaos I. Kanatsoulis, and Jure Leskovec. RelGNN: Composite message passing for relational deep learning. InProc. of ICML. PMLR / OpenReview.net, 2025

    work page 2025

  9. [9]

    On algorithms based on finitely many homomorphism counts.Information and Computation, 306:105326, 2025

    Yijia Chen, Jörg Flum, Mingjun Liu, and Zhiyang Xun. On algorithms based on finitely many homomorphism counts.Information and Computation, 306:105326, 2025

    work page 2025

  10. [10]

    Lovász Meets Weisfeiler and Leman

    Holger Dell, Martin Grohe, and Gaurav Rattan. Lovász Meets Weisfeiler and Leman. InProc. of ICALP, pages 40:1–40:14. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2018

    work page 2018

  11. [11]

    On recognizing graphs by numbers of homomorphisms.Journal of Graph Theory, 64(4):330–342, 2010

    Zdenˇek Dvoˇrák. On recognizing graphs by numbers of homomorphisms.Journal of Graph Theory, 64(4):330–342, 2010

    work page 2010

  12. [12]

    Position: Relational deep learning - graph repre- sentation learning on relational databases

    Matthias Fey, Weihua Hu, Kexin Huang, Jan Eric Lenssen, Rishabh Ranjan, Joshua Robinson, Rex Ying, Jiaxuan You, and Jure Leskovec. Position: Relational deep learning - graph repre- sentation learning on relational databases. InProc. of ICML, pages 13592–13607. PMLR / OpenReview.net, 2024

    work page 2024

  13. [13]

    word2vec, node2vec, graph2vec, x2vec: Towards a theory of vector embeddings of structured data

    Martin Grohe. word2vec, node2vec, graph2vec, x2vec: Towards a theory of vector embeddings of structured data. InProc. of PODS, pages 1–16. ACM, 2020

    work page 2020

  14. [14]

    The logic of graph neural networks

    Martin Grohe. The logic of graph neural networks. InProc. of LICS, pages 1–17. IEEE, 2021

    work page 2021

  15. [15]

    The descriptive complexity of graph neural networks.TheoretiCS, 3, 2024

    Martin Grohe. The descriptive complexity of graph neural networks.TheoretiCS, 3, 2024

    work page 2024

  16. [16]

    A deep graph neural network-based mechanism for social recommendations.IEEE Trans

    Zhiwei Guo and Heng Wang. A deep graph neural network-based mechanism for social recommendations.IEEE Trans. Ind. Informatics, 17(4):2776–2783, 2021

    work page 2021

  17. [17]

    Hamilton, Zhitao Ying, and Jure Leskovec

    William L. Hamilton, Zhitao Ying, and Jure Leskovec. Inductive representation learning on large graphs. InProc. of NeurIPS, pages 1024–1034, 2017

    work page 2017

  18. [18]

    Hauke and Przemyslaw Andrzej Walega

    Stan P. Hauke and Przemyslaw Andrzej Walega. Aggregate-combine-readout GNNs can express logical classifiers beyond the logic C2. InProc. of AAAI, pages 21594–21601. AAAI Press, 2026

    work page 2026

  19. [19]

    Springer Science & Business Media, 2012

    Neil Immerman.Descriptive complexity. Springer Science & Business Media, 2012. 10

    work page 2012

  20. [20]

    Irwin, Teague Sterling, Michael M

    John J. Irwin, Teague Sterling, Michael M. Mysinger, Erin S. Bolstad, and Ryan G. Coleman. ZINC: a free tool to discover chemistry for biology.Journal of chemical information and modeling, 52(7):1757–1768, 2012

    work page 2012

  21. [21]

    Bronstein, ˙Ismail ˙Ilkan Ceylan, and Matthias Lanzinger

    Emily Jin, Michael M. Bronstein, ˙Ismail ˙Ilkan Ceylan, and Matthias Lanzinger. Homomorphism counts for graph neural networks: All about that basis. InProc. of ICML, pages 22075–22098. PMLR / OpenReview.net, 2024

    work page 2024

  22. [22]

    Kipf and Max Welling

    Thomas N. Kipf and Max Welling. Semi-supervised classification with graph convolutional networks. InProc. of ICLR. OpenReview.net, 2017

    work page 2017

  23. [23]

    American Mathematical Soc., 2012

    László Lovász.Large networks and graph limits. American Mathematical Soc., 2012

    work page 2012

  24. [24]

    Unifying approach to uniform expressivity of graph neural networks.arXiv preprint arXiv:2602.18409, 2026

    Huan Luo and Jonni Virtema. Unifying approach to uniform expressivity of graph neural networks.arXiv preprint arXiv:2602.18409, 2026

    work page arXiv 2026

  25. [25]

    The complexity of conjunctive query answering in expressive description logics

    Carsten Lutz. The complexity of conjunctive query answering in expressive description logics. InProc. of IJCAR, number 5195 in LNAI, pages 179–193. Springer, 2008

    work page 2008

  26. [26]

    Deep homomorphism networks

    Takanori Maehara and Hoang NT. Deep homomorphism networks. InProc. of NeurIPS, pages 56076–56107. Curran Associates, Inc., 2024

    work page 2024

  27. [27]

    Weisfeiler and Leman go neural: Higher-order graph neural networks

    Christopher Morris, Martin Ritzert, Matthias Fey, William L Hamilton, Jan Eric Lenssen, Gaurav Rattan, and Martin Grohe. Weisfeiler and Leman go neural: Higher-order graph neural networks. InProc. of AAAI, pages 4602–4609, 2019

    work page 2019

  28. [28]

    Graph homomorphism convolution

    Hoang Nguyen and Takanori Maehara. Graph homomorphism convolution. InProc. of ICML, pages 7306–7316. PMLR, 2020

    work page 2020

  29. [29]

    Ordered subgraph aggregation networks

    Chendi Qian, Gaurav Rattan, Floris Geerts, Mathias Niepert, and Christopher Morris. Ordered subgraph aggregation networks. InProc. of NeurIPS, pages 21030–21045, 2022

    work page 2022

  30. [30]

    Logical characterizations of GNNs with mean aggregation

    Moritz Schönherr and Carsten Lutz. Logical characterizations of GNNs with mean aggregation. InProc. of AAAI. AAAI Press, 2026

    work page 2026

  31. [31]

    Unary negation.Log

    Luc Segoufin and Balder ten Cate. Unary negation.Log. Methods Comput. Sci., 9(3), 2013

    work page 2013

  32. [32]

    A survey of graph neural networks for social recommender systems

    Kartik Sharma, Yeon-Chang Lee, Sivagami Nambi, Aditya Salian, Shlok Shah, Sang-Wook Kim, and Srijan Kumar. A survey of graph neural networks for social recommender systems. ACM Comput. Surv., 56(10):265, 2024

    work page 2024

  33. [33]

    Logical expressiveness of graph neural networks with hierarchical node individualization

    Arie Soeteman and Balder ten Cate. Logical expressiveness of graph neural networks with hierarchical node individualization. InProc. of NeurIPS, 2025

    work page 2025

  34. [34]

    Does GNN pretraining help molecular representa- tion? InProc

    Ruoxi Sun, Hanjun Dai, and Adams Wei Yu. Does GNN pretraining help molecular representa- tion? InProc. of NeurIPS, 2022

    work page 2022

  35. [35]

    Stable tuple embeddings for dynamic databases

    Jan Tönshoff, Neta Friedman, Martin Grohe, and Benny Kimelfeld. Stable tuple embeddings for dynamic databases. InProc. of ICDE, pages 1286–1299. IEEE, 2023

    work page 2023

  36. [36]

    4DBInfer: A 4D benchmarking toolbox for graph-centric predictive modeling on RDBs

    Minjie Wang, Quan Gan, David Wipf, Zheng Zhang, Christos Faloutsos, Weinan Zhang, Muhan Zhang, Zhenkun Cai, Jiahang Li, Zunyao Mao, Yakun Song, Jianheng Tang, Yanlin Zhang, Guang Yang, Chuan Lei, Xiao Qin, Ning Li, Han Zhang, Yanbo Wang, and Zizhao Zhang. 4DBInfer: A 4D benchmarking toolbox for graph-centric predictive modeling on RDBs. In Proc. of NeurIPS, 2024

    work page 2024

  37. [37]

    Structural node embeddings with homomorphism counts.CoRR, abs/2308.15283, 2023

    Hinrikus Wolf, Luca Oeljeklaus, Pascal Kühner, and Martin Grohe. Structural node embeddings with homomorphism counts.CoRR, abs/2308.15283, 2023

    work page arXiv 2023

  38. [38]

    How powerful are graph neural networks? InProc

    Keyulu Xu, Weihua Hu, Jure Leskovec, and Stefanie Jegelka. How powerful are graph neural networks? InProc. of ICLR. OpenReview.net, 2019

    work page 2019

  39. [39]

    Identity-aware graph neural networks

    Jiaxuan You, Jonathan M Gomes-Selman, Rex Ying, and Jure Leskovec. Identity-aware graph neural networks. InProc. of AAAI, pages 10737–10745, 2021

    work page 2021

  40. [40]

    Substructure aware graph neural networks

    DingYi Zeng, Wanlong Liu, Wenyu Chen, Li Zhou, Malu Zhang, and Hong Qu. Substructure aware graph neural networks. InProc. of AAAI, pages 11129–11137. AAAI, 2023. 11 A Additional Material for Section 2 A.1 Missing Definitions We first define some notions introduced in Section 2. Definition 15.TheGaifman graphof anS-databaseDis the undirected graph(V, E), w...

    work page 2023

  41. [41]

    every (connected) GHML − formula is equivalent to a (connected) GHML formula and

    work page

  42. [42]

    on databases of degree at most B, every (connected) GHML formula is equivalent to a (connected) GHML− formula. Proof. We start with Point 1. In view of Lemma 6, it suffices to show that UNFOC can express tuple counting quantifiers φ(¯x) =∃≥n¯y ψ(¯x,¯y).The proof is by induction on the length of ¯y. For |¯y|= 1 there is nothing to do, since UNFOC can quant...

    work page

  43. [43]

    , ym)that is top-level connected

    a formula∃ ≥ℓ1 y1 · · · ∃≥ℓm ym φ′(x, y1, . . . , ym)that is top-level connected

    work page

  44. [44]

    , ym)that are all top-level connected

    formulas∃ ≥ℓ1 y1 · · · ∃≥ℓm ym φ′(y1, . . . , ym)that are all top-level connected

    work page

  45. [45]

    We have already described how to transform the formula in Point 1 into a GHML− formula that is equivalent over all databases of degree at most B

    the formula∃ ≥ky⊤ such that, for distinct formulas, the sets of variables quantified in the outermost quantifier block are disjoint. We have already described how to transform the formula in Point 1 into a GHML− formula that is equivalent over all databases of degree at most B. Each formula ξ in Point 2 can be treated as follows. We first translate ∃≥ℓ2 y...

    work page

  46. [46]

    They don’t choose vertices inCexceptx 3−s

    Duplicatorresponds with vertices according to the sections above. They don’t choose vertices inCexceptx 3−s

    work page

  47. [47]

    Then ind(us)∼ind(u ′ s)iffind(u 3−s)∼ind(u ′ 3−s)for all∼ ∈ {<,=, >}

    Let(u 1, u2),(u ′ 1, u′ 2)be two played pairs which are in the interval[p 1, p2]. Then ind(us)∼ind(u ′ s)iffind(u 3−s)∼ind(u ′ 3−s)for all∼ ∈ {<,=, >}

    work page

  48. [48]

    If x1, x2 ̸∈B i for some i∈ {1,2} : After selecting k vertices, let (u1, u2),(u ′ 1, u′

    work page

  49. [49]

    Then they satisfy: • ifind(u 3−s)̸= ind(u ′ 3−s)then|ind(u 3−s)−ind(u ′ 3−s)| ≥N k, and •|ind(u 3−s)−p i| ≥N k and|p i +N 0 −1−ind(u 3−s)| ≥N k

    be two played pairs such thatu 3−s, u′ 3−s ∈B i. Then they satisfy: • ifind(u 3−s)̸= ind(u ′ 3−s)then|ind(u 3−s)−ind(u ′ 3−s)| ≥N k, and •|ind(u 3−s)−p i| ≥N k and|p i +N 0 −1−ind(u 3−s)| ≥N k

    work page

  50. [50]

    Thenind(u s) = ind(u3−s)

    If x1, x2 ∈B i for some i∈ {1,2} : Let (us, u3−s) be a played pair such that ind(us)∈B i. Thenind(u s) = ind(u3−s). These conditions are obviously satisfied fork= 0. Now let ¯u1 and ¯u2 be tuples with k elements for some 0≤k < n . The game proceeds withSpoiler choosing vertices w(1) s , . . . , w(c′) s , where c′ is at most c.Duplicatornow has to choose c...

    work page

  51. [51]

    for1≤i < nand1≤j≤m:(f(i, j), f(i+ 1, j))∈H

    work page

  52. [52]

    for1≤i≤nand1≤j < m:(f(i, j), f(i, j+ 1))∈V

    work page

  53. [53]

    for1≤j≤m:f(1, j)∈Landf(n, j)∈R

    work page

  54. [54]

    It is shown in [6] that the problem of satisfiable tiling systems is undecidable

    for1≤i≤n:f(i,1)∈Dandf(i, m)∈U. It is shown in [6] that the problem of satisfiable tiling systems is undecidable. We show how to construct a GHML− formulaφ S such that (a) if there is a solution forS, thenφ S is finitely satisfiable in a graph of degree at most 4 and (b) ifφ S is finitely satisfiable, then there is a solution forS. Note that [25] uses a di...

    work page

  55. [55]

    The vertices at the borders are exactly the vertices that have no corresponding neighbor (G(x)∧ ¬B →(x))↔ ∃y 1y2 (E(x, y1)∧H(y 1)∧E(y 1, y2)∧G(y 2)) ∧(G(x)∧ ¬B ←(x))↔ ∃y 1y2 (E(y1, x)∧H(y 1)∧E(y 2, y1)∧G(y 2)) ∧(G(x)∧ ¬B ↑(x))↔ ∃y 1y2 (E(x, y1)∧V(y 1)∧E(y 1, y2)∧G(y 2)) ∧(G(x)∧ ¬B ↓(x))↔ ∃y 1y2 (E(y1, x)∧V(y 1)∧E(y 2, y1)∧G(y 2))

    work page

  56. [56]

    Every grid vertex, that is not on the upper or right border is the origin of a grid cell: (G(x)∧ ¬B ↑(x)∧ ¬B →(x)) → ∃y1y2y3z1z2z3u E(x, y1)∧V(y 1)∧E(y 1, y2)∧G(y 2) ∧E(x, z 1)∧H(z 1)∧E(z 1, z2)∧G(z 2) ∧E(y 2, y3)∧H(y 3)∧E(y 3, u) ∧E(z 2, z3)∧V(z 3)∧E(z 3, u)∧G(u)

    work page

  57. [57]

    The horizontal and vertical grid relations are functional: G(x)→ ¬∃≥2y(E(x, y)∧V(y))∧ ¬∃ ≥2y(E(y, x)∧V(y)) ∧ ¬∃≥2y(E(x, y)∧H(y))∧ ¬∃ ≥2y(E(y, x)∧H(y)) ∧(V(x)∨H(x))→ ¬∃≥2y E(x, y)∧ ¬∃ ≥2y E(y, x)

    work page

  58. [58]

    The borders are consistent: ∀y1y2 (E(x, y1)∨E(y 1, x))∧(E(y 1, y2)∨E(y 2, y1))∧V(y 1) → (B↓(x)↔B ↓(y2))∧(B ↑(x)↔B ↑(y2)) ∧ ∀y1y2 (E(x, y1)∨E(y 1, x))∧(E(y 1, y2)∨E(y 2, y1))∧H(y 1) → (B→(x)↔B →(y2))∧(B ←(x)↔B ←(y2))

    work page

  59. [59]

    Every grid vertex is uniquely tiled: G(x)→ _ t∈T Pt(x)∧ ^ t′∈T\{t} ¬Pt′(x)

    work page

  60. [60]

    The matching conditions are satisfied: (G(x)∧ ¬B ↑(x)) → _ (t,t′)∈V Pt(x)∧ ∃y 1 E(x, y1)∧V(y 1)∧ ∃y 2 (E(y1, y2)∧P t′(y2) ∧(G(x)∧ ¬B →(x)) → _ (t,t′)∈H Pt(x)∧ ∃y 1 E(x, y1)∧H(y 1)∧ ∃y 2 (E(y1, y2)∧P t′(y2) 29

    work page

  61. [61]

    It is routine to verify that φS is a GHML− formula and that it satisfies Condition (a)

    The borders are tiled as required: (B←(x)→ _ t∈L Pt(x))∧(B →(x)→ _ t∈R Pt(x)) ∧(B ↓(x)→ _ t∈D Pt(x))∧(B ↑(x)→ _ t∈U Pt(x)). It is routine to verify that φS is a GHML− formula and that it satisfies Condition (a). We argue that it satisfies Condition (b) as well. Given a model A= (A, G A, V A, HA, B←A, B→A, B↑A , B↓A , EA) we first construct an intermedi- a...

    work page

  62. [62]

    Every (connected) RHML formula is equivalent to a (connected)mean-DHN

    work page

  63. [63]

    let B≥0 ; on databases of degree at most B, every connected RHML formula is equivalent to a connected simplemean-DHN. Proof. We first describe the parts that both points have in common. They will only differ in their combination function for the translation of quantifiers. Letφ be an RHML formula and letφ1, . . . , φk be an enumeration of the subformulas ...

    work page

  64. [64]

    , zk ∈ {x} ∪¯y it either contains R(z1,

    ψ1 is equivalent to a disjunctionW i φi(x,¯y)where each φi is a conjunction such that: • For each relational atom R of arity k and z1, . . . , zk ∈ {x} ∪¯y it either contains R(z1, . . . , zk)or¬R(z 1, . . . , zk)as a conjunct. • For each pair of variables z1, z2 ∈ {x} ∪¯y, it contains either z1 =z 2 or z1 ̸=z 2 as a conjunct. The formula∃¯y ψ(x,¯y)is the...

    work page

  65. [65]

    Spoiler has a winning strategy in theℓ-round UQAFO game when playing on both databases

    work page

  66. [66]

    , xn)with quantifier depth at mostℓsuch that D1 |=φ(v (1) 1 ,

    There exists a UQAFO formulaφ(x 1, . . . , xn)with quantifier depth at mostℓsuch that D1 |=φ(v (1) 1 , . . . , v(n) 1 )⇐ ⇒D 2 ̸|=φ(v (1) 2 , . . . , v(n) 2 ). Proof. We show the implication1.=⇒2. by induction on ℓ. To be more precise, we additionally show that if s is the index of the current configuration then there exists a formula φ(x1, . . . , xn) of ...

    work page

  67. [67]

    Formally atom(v(i) 1 ) = atom(v (i) 2 ) for each 1≤i≤m and ind(v(i) 1 )≤ind(v (j) 1 )↔ ind(v(i) 2 )≤ind(v (j) 2 )for each1≤i, j≤m

    The set of pairs describes a partial isomorphism, that is, the vertices in each pair satisfy the same unary relations and the sets of played vertices is ordered the same in both graphs. Formally atom(v(i) 1 ) = atom(v (i) 2 ) for each 1≤i≤m and ind(v(i) 1 )≤ind(v (j) 1 )↔ ind(v(i) 2 )≤ind(v (j) 2 )for each1≤i, j≤m

    work page

  68. [68]

    Formally, for all1≤i≤m : if ind(v(i) 1 )≤2 ℓ or ind(v(i) 1 )≥2 n+1 −2ℓ+4 or ind(v(i) 2 )≤2 ℓ or ind(v(i) 2 )≥2 n+1 −2ℓ+4, thenind(v (i) 1 ) = ind(v(i) 2 )

    If the configuration contains a vertex near the end of one of the graphs, then the corre- sponding vertex in the other graph has the same position. Formally, for all1≤i≤m : if ind(v(i) 1 )≤2 ℓ or ind(v(i) 1 )≥2 n+1 −2ℓ+4 or ind(v(i) 2 )≤2 ℓ or ind(v(i) 2 )≥2 n+1 −2ℓ+4, thenind(v (i) 1 ) = ind(v(i) 2 )

    work page

  69. [69]

    There are enough vertices satisfyingP, Q, and R between played vertices in G3−s. Formally, for all1≤i, j≤msuch thatind(v (i) s )>ind(v (j) s ),v (i) 3−s andv (j) 3−s satisfy ind(v(i) 3−s)−ind(v (j) 3−s)≥min(2 ℓ,ind(v (i) s )−ind(v (j) s )) +c, where c= ( 1ifind(v (j) 3−s)≤2 n + 1andind(v (i) 3−s)>2 n + 1, 0otherwise. Intuitively, the constantc ensures tha...

    work page

  70. [70]

    and (r2n+1+3 1 , r2n+1+3 2 ) are in C. W.l.o.g. we can also assume that Spoiler does not play a vertex already in some pair of C. Let v(j) s be the played vertex left of xi s, that is, such that ind(v(j) s ) is maximal with ind(v(j) s )< i . Duplicator now responds with xi′ 3−s such that i′ = ind(v(j) 3−s) + min(2ℓ, i−ind(v (j) s )) +c wherecis c= ( 1ifin...

    work page

  71. [71]

    For every GNN with global readoutN,N(G, λ G)(u) =N(H, λ H)(v)

    work page

  72. [72]

    A GNN with global readout and homomorphism count features can be equivalently defined as a DHN of which the first layer has homomorphism queries ((F • 1 , µ,sum),

    For every embedded pointed tree(F •, λ)the following two equalities hold: •|Hom((F •, λ),(G u, λG))|=|Hom((F •, λ),(H v, λH))| •|Hom((F, λ),(G, λ G))|=|Hom((F, λ),(H, λ H))| This result stems from a characterization of the separating power of GNNs as that of the Weisfeiler- Leman algorithm [ 27, 38], and a characterization of the latter as distinguishabil...

    work page

  73. [73]

    , vk) = ¯a; (c) ¯b= (b 1,

    there is a HML+C-term u-itadd(x) such that for all databases D, assignments α over D, anda∈adom(D), Ju-itaddK(D,α)(a) = X ¯a¯b α(U)(¯a¯b), where the sum ranges over all ¯a¯b∈adom(D) k ×N ℓ such that the following conditions are satisfied: (a)¯a¯b∈α(X); (b) there is a homomorphismhfromFtoDwithh(v 1) =aandh(v 1, . . . , vk) = ¯a; (c) ¯b= (b 1, . . . , bℓ)∈N...

    work page

  74. [74]

    there are HML+C-termsu-max(x) and u-min(x) such that for all databasesD, assignments αoverD, anda∈adom(D), Ju-maxK(D,α)(a) =max ¯a¯bα(U)(¯a)andJu-minK (D,α)(a) = min ¯a¯b α(U)(¯a) where max and min range over all ¯a¯b∈adom(D) k ×N ℓ that satisfy Conditions (a)-(c) from Point 1. Proof. To simplify notation, in the proof we assume that ℓ= 1 . The generaliza...

    work page 1921