arxivcs.LOcs.AI2026-07-23
Towards a Certifying Grounder
Daimy Van Caudenberg, Alexander Ek, Carlos Cantero, Bart Bogaerts
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 s…