Доказательство теоремы Бельтюкова - Липшица квазиэлиминацией кванторов. II. Основное сведение
DOI:
https://doi.org/10.21638/spbu01.2021.406Аннотация
Работа является второй частью нового доказательства теоремы Бельтюкова-Липшица о разрешимости экзистенциальной теории структуры . Строится алгоритм квази-ЭК (понятие введено в первой части доказательства), осуществляющий сведение проблемы разрешимости для экзистенциальной теории структуры к проблеме разрешимости для позитивной экзистенциальной теории структуры 0; 1, {a·}a∈Z>0 , НОД>. Так как разрешимость последней теории была доказана в первой части, построенное сведение завершит доказательство теоремы. На шаге отделения переменной для квазиэлиминации используются аналоги двух лемм из доказательства Липшица. Шаг квазиэлиминации основан на НОДлемме, доказанной в первой части.Ключевые слова:
элиминация кванторов, экзистенциальная теория, делимость, алгоритмическая разрешимость, китайская теорема об остатках
Скачивания
Данные скачивания пока недоступны.
Библиографические ссылки
Литература
1. Бельтюков А.П. Разрешимость универсальной теории натуральных чисел со сложением и делимостью. Записки научных семинаров ЛОМИ 60, 15–28 (1975).
2. Lipshitz L. The Diophantine problem for addition and divisibility. Transactions of the American Mathematical Society 235, 271–283 (1978). https://doi.org/10.1090/S0002-9947-1978-0469886-1
3. Старчак М.Р. Доказательство теоремы Бельтюкова - Липшица квазиэлиминациейкванторов. I. Определения и НОД-лемма. Вестник Санкт-Петербургского университета. Математика. Механика. Астрономия 8 (66), вып. 3, 455–466 (2021). https://doi.org/10.21638/spbu01.2021.307
4. Lechner A., Ouaknine J., Worrell J. On the complexity of linear arithmetic with divisibility. Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 667– 676 (2015). https://doi.org/10.1109/LICS.2015.67
5. von zur Gathen J., Sieveking M. A bound on solutions of linear integer equalities and inequalities. Proceedings of the American Mathematical Society 72, iss. 1, 155–158 (1978). https://doi.org/10.2307/2042554
6. Barth D., Beck M., Dose T., Glaßer C., Michler L., Technau M. Emptiness problems for integer circuits. Electronic Colloquium on Computational Complexity, TR17-012 (2017). Доступно на: https://eccc.weizmann.ac.il/report/2017/012/ (дата обращения: 25.08.2021).
7. Mostowski A. On direct products of theories. The Journal of Symbolic Logic 17, iss. 1, 1–31 (1952). https://doi.org/10.2307/2267454
References
1. Bel’tyukov A.P. Decidability of the Universal Theory of the Natural Numbers with Addition and Divisibility. Zapiski Nauchnyh Seminarov LOMI 60, 15–28 (1976). (In Russian)
2. Lipshitz L. The Diophantine problem for addition and divisibility. Transactions of the American Mathematical Society 235, 271–283 (1978). https://doi.org/10.1090/S0002-9947-1978-0469886-1
3. Starchak M.R. A proof of Bel’tyukov - Lipshitz theorem by quasi-quantifier elimination. I. Definitions and GCD-lemma. Vestnik of Saint Petersburg University. Mathematics. Mechanics. Astronomy 8 (66), iss. 3, 455–466 (2021). https://doi.org/10.21638/spbu01.2021.307 (In Russian) [Engl. transl.: Vestnik St. Petersb. Univ. Math. 54, iss. 3, 264–272 (2021). https://doi.org/10.1134/S1063454121030080].
4. Lechner A., Ouaknine J., Worrell J. On the complexity of linear arithmetic with divisibility. Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 667–676 (2015). https://doi.org/10.1109/LICS.2015.67
5. von zur Gathen J., Sieveking M. A bound on solutions of linear integer equalities and inequalities. Proceedings of the American Mathematical Society 72, iss. 1, 155–158 (1978). https://doi.org/10.2307/2042554
6. Barth D., Beck M., Dose T., Glaßer C., Michler L., Technau M. Emptiness problems for integer circuits. Electronic Colloquium on Computational Complexity, TR17-012 (2017). Available at: https://eccc.weizmann.ac.il/report/2017/012/ (accessed: August 25, 2021).
7. Mostowski A. On direct products of theories. The Journal of Symbolic Logic 17, iss. 1, 1–31 (1952). https://doi.org/10.2307/2267454
Загрузки
Опубликован
04.01.2022
Как цитировать
Старчак, М. Р. (2022). Доказательство теоремы Бельтюкова - Липшица квазиэлиминацией кванторов. II. Основное сведение. Вестник Санкт-Петербургского университета. Математика. Механика. Астрономия, 8(4), 608–619. https://doi.org/10.21638/spbu01.2021.406
Выпуск
Раздел
Математика
Лицензия
Статьи журнала «Вестник Санкт-Петербургского университета. Математика. Механика. Астрономия» находятся в открытом доступе и распространяются в соответствии с условиями Лицензионного Договора с Санкт-Петербургским государственным университетом, который бесплатно предоставляет авторам неограниченное распространение и самостоятельное архивирование.
