# Towards a Certifying Grounder

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 7 of its 40 references that are in the map.
- First posted on arXiv 23 Jul 2026.

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

- [Certified Symmetry and Dominance Breaking for Combinatorial Optimisation](https://mlsanity.com/paper/2203.12275/) (2022)
- [Grounding FO and FO(ID) with Bounds](https://mlsanity.com/paper/1401.3840/) (2014)
- [Certified MaxSAT Preprocessing](https://mlsanity.com/paper/2404.17316/) (2024)
- [Inconsistency Proofs for ASP: The ASP-DRUPE Format](https://mlsanity.com/paper/1907.10389/) (2019)
- [Certifying Pareto-Optimality in Multi-Objective Maximum Satisfiability](https://mlsanity.com/paper/2501.17493/) (2025)
- [Efficient and Reliable Hitting-Set Computations for the Implicit Hitting Set Approach](https://mlsanity.com/paper/2508.07015/) (2025)
- [Using Certifying Constraint Solvers for Generating Step-wise Explanations](https://mlsanity.com/paper/2511.10428/) (2025)

## Abstract (arXiv)

Grounding, the translation of high-level theories into equivalent quantifier-free formulas, is a crucial step in declarative solving, yet it has so far escaped the proof-logging revolution. When this grounding step is not certifying, there is no way of knowing that the obtained solutions actually correspond to the original problem specification, resulting in a trust gap. In this paper, we close the trust gap between the user's high-level specification and the solver's low-level input by introducing a novel certifying grounding framework for first-order logic model expansion (FOX) over finite domains. We present CertiFOX, a framework consisting of: (1) a proof format for grounding derivations, (2) GroundFOX, a certifying grounder operating on theories in Grounding Normal Form (GNF)--a new normal form designed for compact, domain-aware grounding--and (3) CheckFOX, an independent proof checker. Our approach guarantees that the grounder's output is equivalent to the input specification, setting the stage for trustworthy end-to-end certified solving pipelines for declarative languages. Experimental evaluation confirms that CertiFOX is a feasible approach. The GroundFOX grounder is broadly comparable with other grounders, and proof checking with CheckFOX adds overhead within a small constant factor of grounding time.