On computational complexity of successor theory with unary transitive closure
Sergey Mikhailovich Dudakov · Journal of Physics Conference Series · 2019
The present article concerns the theory of the successor function with the unary transitive closure (TC) operator. This theory is equivalent to the TC-theory of discrete linear order with respect to TC-definability. We prove that any decision algorithm for this theory has at least hyperexponential computational complexity. The latter is much higher than the complexity of the same theories without the TC-operator.