将合并归结拓展至一族证明系统

合并归结(MRes [Beyersdorff et al. J. Autom. Reason.'2021])是最近引入的用于假QBF的证明系统。它将反模型存储为合并映射。合并映射是确定性分支程序，其中同构检查是高效的，使得MRes成为多项式时间可验证的证明系统。在本文中，我们引入一族证明系统MRes-R，其中反模型存储于任意预先固定的完全表示R中，而非合并映射。因此对应于每个这样的R，我们在MRes-R中拥有一个可靠且反驳完全的QBF证明系统。为处理策略的任意表示，我们在MRes-R中引入一致性检查规则以取代同构检查。结果这些证明系统不是多项式时间可验证的。因此，本文表明使用合并映射过于受限，可被任意表示替代，从而产生若干有趣的证明系统。探索MRes-R的证明论性质，我们展示了eFrege+$\forall$red模拟MRes-R中证明系统的所有有效反驳。为模拟MRes-R中的任意表示，我们首先将证明系统所用的步骤表示为一种新的完全结构。相应地，属于MRes-R的对应证明系统能够模拟MRes-R中的所有证明系统。最后，我们利用[Chew et al. ECCC.'2021]中的思想通过eFrege+$\forall$red模拟该证明系统。在下界方面，我们展示了来自[Jonata et al. Theor. Comput. Sci.'2015]的完成原理公式——其在[Beyersdorff et al. FSTTCS.'2020]中被证明对正则MRes是困难的——也对MRes-R中任意正则证明系统是困难的。从而，本文将正则MRes的下界提升到了一整类使用某种完全表示（包括那些尚未发现的，而非合并映射）的证明系统。