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

Voir la notice de l'article provenant de la source Math-Net.Ru

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},
     publisher = {mathdoc},
     number = {3},
     year = {2016},
     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
PB  - mathdoc
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
%I mathdoc
%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/