We propose a modal logic in which counting modalities appear in linear
inequalities. We show that each formula can be transformed into an equivalent
graph neural network (GNN). We also show that a broad class of GNNs can be
transformed efficiently into a formula, thus significantly improving upon the
literature about the logical expressiveness of GNNs. We also show that the
satisfiability problem is PSPACE-complete. These results bring together the
promise of using standard logical methods for reasoning about GNNs and their
properties, particularly in applications such as GNN querying, equivalence
checking, etc. We prove that such natural problems can be solved in polynomial
space.

提出了一种模态逻辑，在其中计数模态出现在线性不等式中。将每个公式转换为等价的图神经网络（GNN）。证明了广泛类别的 GNN 可以高效地转换为公式，从而明显改进了关于 GNN 的逻辑表达能力的文献。证明了可满足性问题的 PSPACE 完备性。这些结果将常规逻辑方法和 GNN 及其属性的推理前景结合起来，尤其适用于 GNN 查询、等价性检查等应用。证明了这种自然问题可以在多项式空间内解决。

关于聚合组合图神经网络推理的逻辑

A Logic for Reasoning About Aggregate-Combine Graph Neural Networks

Graph Neural Networks (GNNs) have been recently introduced to learn from
knowledge graph (KG) and achieved state-of-the-art performance in KG reasoning.
However, a theoretical certification for their good empirical performance is
still absent. Besides, while logic in KG is important for inductive and
interpretable inference, existing GNN-based methods are just designed to fit
data distributions with limited knowledge of their logical expressiveness. We
propose to fill the above gap in this paper. Specifically, we theoretically
analyze GNN from logical expressiveness and find out what kind of logical rules
can be captured from KG. Our results first show that GNN can capture logical
rules from graded modal logic, providing a new theoretical tool for analyzing
the expressiveness of GNN for KG reasoning; and a query labeling trick makes it
easier for GNN to capture logical rules, explaining why SOTA methods are mainly
based on labeling trick. Finally, insights from our theory motivate the
development of an entity labeling method for capturing difficult logical rules.
Experimental results are consistent with our theoretical results and verify the
effectiveness of our proposed method.

本文从逻辑表达式的角度对图神经网络进行了理论分析，实验结果验证了我们提出的实体标记方法的有效性，并揭示了基于标记技巧的最先进的方法为什么很有效。