摘要
arXiv:2502.12278v1 公告类型: cross
摘要: 一阶模型计数(FOMC)是计算一阶逻辑句子的模型数量的问题。由于提升推理技术依赖于FOMC的各种变体,因此在过去十年中,理论工作者和实践者都关注于设计可扩展的FOMC方法。最近,提出了一种基于一阶知识编译的新方法。该方法称为Crane,它不仅提供了最终计数,还生成了(可能递归的)函数的定义,这些函数可以接受不同的参数来计算任何领域大小的模型计数。然而,这种方法并非完全自动化,因为它需要手动评估构建的函数。本文的主要贡献是一种完全自动化的编译算法,称为Gantry,该算法将函数定义转换为配备了任意精度算术的C++代码。这些添加使得新的FOMC算法能够扩展到比当前最先进的技术大50多万倍的领域大小,实验结果证明了这一点。