arXiv:2405.00205v2 宣告类型: 替换 摘要: 我们提出了一种模态逻辑，在这种逻辑中，计数模态出现在线性不等式中。我们展示了一个公式可以被转换成等价的图形神经网络（GNN）。我们还展示了可以高效地将广泛的GNN类转换为公式，从而显著改善了关于GNN逻辑表达能力的文献。此外，我们展示了可满足性问题是PSPACE完全的。这些结果将利用标准逻辑方法来推理GNN及其属性的前景汇聚在一起，特别是在GNN查询、等价性检查等应用方面。我们证明了这类自然问题可以在多项式空间中解决。