Проект посвящён проблемам, решение которых имело бы высокую ценность во всякое время с того момента, как Пресбургером была доказана разрешимость арифметики сложения натуральных чисел в 1929 году. Однако, интерес к такого рода вопросам в определённые моменты ослабевал ввиду трудностей в дальнейшем продвижении в ключевых вопросах этой области. Новый виток активного изучения вопросов разрешимости и выразимости в арифметических структурах приходится на последние 10-5 лет, когда в работах различных групп исследователей был получен ряд фундаментальных результатов, и были поставлены совершенно новые проблемы.
В первую очередь стоит отметить работу Christoph Haase (https://www.cs.ox.ac.uk/people/christoph.haase/home/), инициировавшего в 2020 году проект ARiAT (Advanced Reasoning in Arithmetic Theories https://www.cs.ox.ac.uk/people/christoph.haase/home/project/ariat/). Кроме того, в прошедшем году на конференции ICALP был организован семинар под названием "Trends in Arithmetic Theories", на котором исследователями представляются их достижения в вопросах арифметических теорий. Задачи, которые предполагается решить в рамках данного проекта, входят в широкий контекст исследований проекта ARiAT. В то же время, методы, которыми предполагается осуществлять исследования, ближе к работам французских математиков таких как Alexis Bès из LACL (Laboratoire d’Algorithmique, Complexité et Logique) или Françoise Point из Université de Mons. Эти методы восходят к фундаментальным работам А.Л. Семёнова.
Значительного прогресса в вопросах разрешимых расширений арифметики Пресбургера удалось достичь Philipp Hieronymi (https://www.math.uni-bonn.de/people/phierony/). С помощью автоматного подхода им были получены результаты о разрешимости и неразрешимости для расширений с помощью функций умножения на вещественные скаляры. Как сказано в пункте 4.5 ниже, в 2022 году ему удалось решить совместно со своим аспирантом Christian Schulz старую открытую проблему и тем самым открыть много новых вопросов о разрешимости. Кроме того, его группа активно развивает средство автоматического доказательства теорем Pecan, которое позволяет автоматизировать доказательство теорем в расширении арифметики Пресбургера регулярными языками. Этот инструмент основан на его аналоге -- Walnut, получившем большую популярность в последнее время благодаря работам Jeffrey O. Shallit (https://cs.uwaterloo.ca/~shallit/). В 2022 году им была опубликована монография "The Logical Approach To Automatic Sequences" (https://cs.uwaterloo.ca/~shallit/walnut-book.html) посвящённая Walnut и k-регулярным языкам.
Отправной точкой исследования являются следующие работы автора проекта по экзистенциальным арифметикам:
1) Starchak, M.R. 2023. On the Existential Arithmetics with Addition and Bitwise Minimum. In Proceedings of the 26th International Conference on Foundations of Software Science and Computation Structures. FoSSaCS 2023. Lecture Notes in Computer Science, vol 13992, 176–195. https://doi.org/10.1007/978-3-031-30829-1_9
2) Mikhail R. Starchak. 2022. Quasi-Quantifier Elimination Algorithms and Definability Problems in Arithmetics with Divisibility. PhD Thesis. St. Petersburg University. https://disser.spbu.ru/files/2022/disser_starchak.pdf
3) Mikhail R. Starchak. 2021. Positive Existential Definability with Unit, Addition and Coprimeness. In Proceedings of the 2021 on International Symposium on Symbolic and Algebraic Computation (ISSAC '21). Association for Computing Machinery, New York, NY, USA, 353–360. https://doi.org/10.1145/3452143.3465515
4) Starchak, M.R. A Proof of Bel’tyukov–Lipshitz Theorem by Quasi-Quantifier Elimination. II. The Main Reduction. Vestnik St.Petersb. Univ.Math. 54, 372–380 (2021). https://doi.org/10.1134/S106345412104018X
5) Starchak, M.R. A Proof of Bel’tyukov–Lipshitz Theorem by Quasi-Quantifier Elimination. I. Definitions and GCD-Lemma. Vestnik St.Petersb. Univ.Math. 54, 264–272 (2021). https://doi.org/10.1134/S1063454121030080
