发表机构
KU Leuven, Leuven, Belgium ARC Training Centre OPTIMA, Melbourne, Australia（比利时列日大学 澳大利亚OPTIMA培训中心）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
研究为一阶逻辑模型扩展引入可验证基础化框架CertiFOX，含证明格式、基础器GroundFOX和证明检查器CheckFOX，弥合用户规范与求解器输入的信任差距，保证输出与输入等价，实验表明该方法可行。
AI 中文摘要
基础化，即将高级理论转换为等价的无量词公式，是声明式求解中的关键步骤，但至今尚未融入证明记录变革。当此基础化步骤不可验证时，无法知晓所得解是否真正对应原始问题规范，导致信任差距。本文通过为有限域上的一阶逻辑模型扩展（FOX）引入一种新颖的可验证基础化框架，弥合了用户高级规范与求解器低级输入之间的信任差距。我们展示了CertiFOX，一个由以下部分组成的框架：（1）基础化推导的证明格式；（2）GroundFOX，一个对处于基础化范式（GNF）——一种为紧凑的、域感知基础化设计的新范式——的理论进行操作的可验证基础器；（3）CheckFOX，一个独立的证明检查器。我们的方法保证基础器的输出等同于输入规范，为声明式语言可靠的端到端可验证求解管道奠定基础。实验评估证实CertiFOX是一种可行的方法。GroundFOX基础器与其他基础器大致可比，并且用CheckFOX进行证明检查在基础化时间的小常数因子范围内增加了开销。
英文摘要
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.
CommentsIn Proceedings ICLP 2026, arXiv:2607.17707
Journal refEPTCS 450, 2026, pp. 309-324
