Grounding Normal Form

新的CertiFOX框架确保声明式求解的可信归纳

研究人员推出CertiFOX，一个旨在确保声明式求解过程可信度的新框架。该框架通过提供一个认证式归纳器GroundFOX来弥合“信任鸿沟”，GroundFOX将高级理论转换为无量词公式。配套的证明检查器CheckFOX验证原始规范与归纳器的输出之间的等价性，从而实现可靠的端到端认证求解流水线。实验结果表明，CertiFOX是一种实用的方法，GroundFOX的性能与现有归纳器相当，而CheckFOX的开销极小。