# Axiomatic Foundations and Algorithms for Deciding Semantic Equivalences of SQL Queries

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

## Key facts

- Cited by 11 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 6 Feb 2018.

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

- [LLM-SQL-Solver: Can LLMs Determine SQL Equivalence?](https://mlsanity.com/paper/2312.10321/) (2023)
- [SpotIt: Evaluating Text-to-SQL Evaluation with Formal Verification](https://mlsanity.com/paper/2510.26840/) (2025)
- [LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4](https://mlsanity.com/paper/2507.14722/) (2025)
- [Can the Rookies Cut the Tough Cookie? Exploring the Use of LLMs for SQL Equivalence Checking](https://mlsanity.com/paper/2412.05561/) (2024)
- [GEqO: ML-Accelerated Semantic Equivalence Detection](https://mlsanity.com/paper/2401.01280/) (2024)
- [FuncEvalGMN: Evaluating Functional Correctness of SQL via Graph Matching Network](https://mlsanity.com/paper/2407.14530/) (2024)
- [SpotIt+: Verification-based Text-to-SQL Evaluation with Database Constraints](https://mlsanity.com/paper/2603.04334/) (2026)
- [SQLStructEval: Structural Evaluation of LLM Text-to-SQL Generation](https://mlsanity.com/paper/2604.06736/) (2026)
- [An Automated SQL Query Grading System Using An Attention-Based Convolutional Neural Network](https://mlsanity.com/paper/2406.15936/) (2024)
- [Polygon: Symbolic Reasoning for SQL using Conflict-Driven Under-Approximation Search](https://mlsanity.com/paper/2504.06542/) (2025)
- [AutoIndexer: A Reinforcement Learning-Enhanced Index Advisor Towards Scaling Workloads](https://mlsanity.com/paper/2507.23084/) (2025)

## Abstract (arXiv)

Deciding the equivalence of SQL queries is a fundamental problem in data management. As prior work has mainly focused on studying the theoretical limitations of the problem, very few implementations for checking such equivalences exist. In this paper, we present a new formalism and implementation for reasoning about the equivalences of SQL queries. Our formalism, U-semiring, extends SQL's semiring semantics with unbounded summation and duplicate elimination. U-semiring is defined using only very few axioms and can thus be easily implemented using proof assistants such as Coq for automated query reasoning. Yet, they are sufficient enough to enable us reason about sophisticated SQL queries that are evaluated over bags and sets, along with various integrity constraints. To evaluate the effectiveness of U-semiring, we have used it to formally verify 39 query rewrite rules from both classical data management research papers and real-world SQL engines, where many of them have never been proven correct before.