Geodesic
On the lower bondary for time complexity of a decidability problem of a theory of integers with a successor function and the least fixed point operator
Vestnik Tverskogo gosudarstvennogo universiteta. Seriâ Prikladnaâ matematika, no. 3 (2016), pp. 97-109 Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice de l'article

We show that any decision procedure for the theory of integers with a successor function and a least fixed point operator for a formula with $n$ nested operators has at least hyperexponential time complexity. There are two stages in the proof. First of all we show that an exponential shift can be represented using short formulas. We construct least fixed point operator which enumerates binary codes of initial segment of natural numbers. Then we show that cellular automation with hyperexponential time complexity can be modeled using least fixed point operator. We also note that the final formula length is linear dependent on the input data length.
Keywords: decidability, fixed point operator, time complexity. 
@article{VTPMK_2016_3_a7,
     author = {A. S. Zolotov},
     title = {On the lower bondary for time complexity of a decidability problem of a theory of integers with a successor function and the least fixed point operator},
     journal = {Vestnik Tverskogo gosudarstvennogo universiteta. Seri\^a Prikladna\^a matematika},
     pages = {97--109},
     year = {2016},
     number = {3},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/VTPMK_2016_3_a7/}
}
TY  - JOUR
AU  - A. S. Zolotov
TI  - On the lower bondary for time complexity of a decidability problem of a theory of integers with a successor function and the least fixed point operator
JO  - Vestnik Tverskogo gosudarstvennogo universiteta. Seriâ Prikladnaâ matematika
PY  - 2016
SP  - 97
EP  - 109
IS  - 3
UR  - http://geodesic.mathdoc.fr/item/VTPMK_2016_3_a7/
LA  - ru
ID  - VTPMK_2016_3_a7
ER  - 
%0 Journal Article
%A A. S. Zolotov
%T On the lower bondary for time complexity of a decidability problem of a theory of integers with a successor function and the least fixed point operator
%J Vestnik Tverskogo gosudarstvennogo universiteta. Seriâ Prikladnaâ matematika
%D 2016
%P 97-109
%N 3
%U http://geodesic.mathdoc.fr/item/VTPMK_2016_3_a7/
%G ru
%F VTPMK_2016_3_a7
A. S. Zolotov. On the lower bondary for time complexity of a decidability problem of a theory of integers with a successor function and the least fixed point operator. Vestnik Tverskogo gosudarstvennogo universiteta. Seriâ Prikladnaâ matematika, no. 3 (2016), pp. 97-109. http://geodesic.mathdoc.fr/item/VTPMK_2016_3_a7/

[1] Dudakov S. M., “On inflationary fix-point operators safety”, Lobachevskii Journal of Mathematics, 36:4 (2015), 328–331 | DOI | MR | Zbl

[2] Fischer M. J., Rabin M. O., “Super-Exponential Complexity of Presburger Arithmetic”, Proceedings of the SIAM-AMS Symposium in Applied Mathematics, v. 7, 1974, 27–41 | MR | Zbl

[3] Gurevich Y., Shelah S., “Fixed-point extensions of first-order logic”, Annals of Pure and Applied Logic, 32 (1986), 265–280 | DOI | MR | Zbl

[4] Rogers H., Theory of Recursive Functions and Effective Computability, MIT Press, 1972 (in Russian) | MR

[5] Snyatkov A. S., “Lower boundary of time to resolve the theory with the exponential function”, Vestnik TvGU. Seriya: Prikladnaya Matematika [Herald of Tver State University. Series: Applied Mathematics], 2012, no. 2(25), 5–10 (in Russian)