关于三次齐次方程可满足性的考察

我们的贡献是一种有界三次编译定理。对于每个固定的资源参数 $k$，在资源水平 $k$ 上的语法证明检查被忠实地表示为一个有限的有界域三次多项式方程组。每个产生的方程最高次数至多为 3。三次项仅在线性选择变量激活二次验证义务时才会出现。本文的早期版本曾声称将无限制的theoremhood 归约到满足固定有界域三次多项式实例的可满足性。该论点已撤回。准确指出了该错误及其来源。该有界构造、次数记录以及基于 Zeckendorf 的无进位编码均独立于已撤回的论点而存在。本文最后指出了将一族可判定的有界切片与单个多对一归约目标分隔开的均匀化间隙，并记录了为何需要压缩原理才能弥合该间隙，而该原理在本文中并未提供。