自动定理证明中的罕见加速揭示计算时间与信息价值之间的权衡

我们展示了自动定理证明中实现的策略涉及执行速度、证明加速/计算时间与信息有用性之间的有趣权衡。我们通过与添加有用信息（其他定理作为公理）时期望的（最优）理论加速相关的“正态性”概念，推进这些概念的正式定义，并与可有效高效实施的实际策略相比较。我们提出在此正态性与计算时间复杂性之间存在不可避免的权衡。该论证根据（正）加速量化信息的有用性。结果揭示了一种“没有免费午餐”的情形及本质性的权衡。本文的主定理连同数值实验——使用两种不同的自动定理证明器 AProS 和 Prover9 对命题逻辑的随机定理进行——为如下事实提供了强有力的理论与经验论据：一般而言，为求解特定问题（定理）寻找新的有用信息与问题（定理）本身同样困难。