Towards a Certifying Grounder

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 GROUND-FOX grounder is broadly comparable with other grounders, and proof checking with CHECKFOX adds overhead within a small constant factor of grounding time.