期刊名称：Electronic Colloquium on Computational Complexity
印刷版ISSN：1433-8092
出版年度：2021
卷号：21
语种：English
出版社：Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
摘要：We call any consistent and sufficiently powerful formal theory that enables to algorithmically verify whether a text is a proof \textbf{algorithmically verifiable mathematics} (av-mathematics). We study the question whether nondeterminism is more powerful than determinism for polynomial time computations in the framework of av-mathematics. Our main results are as follows. \\ "\P\subsetneq\NP or for any deterministic, polynomial time compression algorithm A there exists a nondeterministic, polynomial time compression machine M that reduces infinitely many binary strings logarithmically stronger than A." \\ "\P\subsetneq\NP or f-time resource bounded Kolmogorov complexity of any binary string x can be computed in deterministic polynomial time for each polynomial, time constructible function f."\\ For computing models with "efficient" interpreters we prove the following theorem:\\ "For each polynomial, time constructible function f, \TIMEf\subsetneq\NTIMEf or one can essentially stronger compress words nondeterministically in time \Ohf(n) than deterministically in time f(n)."
