# A Logic for Reasoning About Aggregate-Combine Graph Neural Networks

arXiv: https://arxiv.org/abs/2405.00205 · HTML: https://mlsanity.com/paper/2405.00205/

## Key facts

- Cited by 10 papers in the map (data through 14 Oct 2026).
- Builds on 9 of its 37 references that are in the map.
- First posted on arXiv 30 Apr 2024.

## Builds on (most cited first, 9 of 9)

- [Neural Message Passing for Quantum Chemistry](https://mlsanity.com/paper/1704.01212/) (2017)
- [Graph Neural Networks: A Review of Methods and Applications](https://mlsanity.com/paper/1812.08434/) (2018)
- [Explainability in Graph Neural Networks: A Taxonomic Survey](https://mlsanity.com/paper/2012.15445/) (2020)
- [Graph neural networks for materials science and chemistry](https://mlsanity.com/paper/2208.09481/) (2022)
- [The Logic of Graph Neural Networks](https://mlsanity.com/paper/2104.14624/) (2021)
- [Global Explainability of GNNs via Logic Combination of Learned Concepts](https://mlsanity.com/paper/2210.07147/) (2022)
- [On the Correspondence Between Monotonic Max-Sum GNNs and Datalog](https://mlsanity.com/paper/2305.18015/) (2023)
- [DT+GNN: A Fully Explainable Graph Neural Network using Decision Trees](https://mlsanity.com/paper/2205.13234/) (2022)
- [Satisfiability and Query Answering in Description Logics with Global and Local Cardinality Constraints](https://mlsanity.com/paper/2002.06072/) (2020)

## Built on by (most cited first, 10 of 10)

- [Exact Verification of Graph Neural Networks with Incremental Constraint Solving](https://mlsanity.com/paper/2508.09320/) (2025)
- [Verifying Quantized Graph Neural Networks is PSPACE-complete](https://mlsanity.com/paper/2502.16244/) (2025)
- [The Logical Expressiveness of Temporal GNNs via Two-Dimensional Product Logics](https://mlsanity.com/paper/2505.11930/) (2025)
- [Sound Logical Explanations for Mean Aggregation Graph Neural Networks](https://mlsanity.com/paper/2511.11593/) (2025)
- [DeepGraphLog for Layered Neurosymbolic AI](https://mlsanity.com/paper/2509.07665/) (2025)
- [From Neural Networks to Logical Theories: The Correspondence between Fibring Modal Logics and Fibring Neural Networks](https://mlsanity.com/paper/2509.23912/) (2025)
- [Robustness Verification of Graph Neural Networks Via Lightweight Satisfiability Testing](https://mlsanity.com/paper/2510.18591/) (2025)
- [Clausal Deletion Backdoors for QBF: a Parameterized Complexity Approach](https://mlsanity.com/paper/2605.12073/) (2026)
- [Structural Preservation and the Logical Expressiveness of Graph Neural Networks](https://mlsanity.com/paper/2606.17882/) (2026)
- [Beyond Trained Models: Compiling GNNs for a Sound Explainer Benchmark](https://mlsanity.com/paper/2610.03526/) (2026)

## Abstract (arXiv)

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.