计算机运行时间与证明长度：关于算法概率在自动定理证明等待时间中的应用
计算复杂性
2012-01-05 v1 计算机科学中的逻辑
逻辑
摘要
本文是对 Turing 机的运行时间与形式公理系统中证明长度之间关系的实验性探索。我们将给定规模的停机 Turing 机数量与给定规模的一阶逻辑可证明定理数量进行比较，并将给定规模中运行时间最长的 Turing 机的运行时间与给定规模中最难证明的定理的证明长度进行比较。研究表明，定理证明器与计算机程序一样，受制于时间与规模之间相同的非线性权衡，这为在自动定理证明中确定最佳超时与等待时间提供了可能。我提供了这两个系统在一些小参数选择下的统计数据。
引用
@article{arxiv.1201.0825,
title = {Computer Runtimes and the Length of Proofs: On an Algorithmic Probabilistic Application to Waiting Times in Automatic Theorem Proving},
author = {Hector Zenil},
journal= {arXiv preprint arXiv:1201.0825},
year = {2012}
}
备注
forthcoming in M.J. Dinneen, B Khoussainov and A. Nies (eds), "Computation, Physics and Beyond", LNCS, Springer (Cristian S. Calude festschrift)