Доказательство теоремы Бельтюкова-Липшица квазиэлиминацией кванторов. I. Определения и НОД-лемма
DOI:
https://doi.org/10.21638/spbu01.2021.307Аннотация
Данная работа является первой частью нового доказательства разрешимости экзистенциальной теории структуры , где | соответствует двухместному отношению делимости. Разрешимость этой теории была доказана в 1976 г. независимо А.П. Бельтюковым и Л.Липшицем. В 1977 г. В. И.Мартьянов получил эквивалентный результат, рассматривая трехместный предикат НОД вместо отношения делимости (эти предикаты экзистенциально выражаются друг через друга с помощью других символов сигнатуры). В работе вводится понятие алгоритма квазиэлиминации кванторов (квази-ЭК), обобщающее в некотором смысле понятие алгоритма элиминации кванторов, а затем строится алгоритм квази-ЭК для позитивной экзистенциальной теории структуры <...>. К проблеме разрешимости для этой теории сводится проблема разрешимости для экзистенциальной теории структуры <...>. Алгоритм квази-ЭК, осуществляющий такое сведение, будет построен во второй части доказательства. Преобразования формул основаны на обобщении китайской теоремы об остатках для систем вида НОД(ai, bi + x) = di для всех i [1..m], где ai, bi, di - целые числа, такие что ai 6= 0, di > 0.Ключевые слова:
элиминация кванторов, экзистенциальная теория, делимость, алгоритмическая разрешимость, китайская теорема об остатках
Скачивания
Данные скачивания пока недоступны.
Библиографические ссылки
Литература
1. Бельтюков А.П. Разрешимость универсальной теории натуральных чисел со сложением и делимостью. Записки научных семинаров ЛОМИ 60, 15–28 (1976).
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. Мартьянов В.И. Универсальные расширенные теории целых чисел. Алгебра и логика 16 (5), 588–602 (1977).
4. Lipshitz L. Some remarks on the Diophantine problem for addition and divisibility. Bull. Soc. Math. Belg. Ser. B 33, iss. 1, 41–52 (1981).
5. 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
6. Weispfenning V. The complexity of linear problems in fields. Journal of Symbolic Computation 5, iss. 1–2, 3–27 (1988). https://doi.org/10.1016/S0747-7171(88)80003-8
7. Gu´epin F., Haase C., Worrell J. On the existential theories of B¨uchi arithmetic and linear p-adic fields. Proceedings of the 34th Annual ACM / IEEE Symposium on Logic in Computer Science (LICS), 1–10 (2019). https://doi.org/10.1109/LICS.2019.8785681
8. Schmid H. L., Mahler K. On the Chinese remainder theorem. Mathematische Nachrichten 18, 120–122 (1958).
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. Mart’yanov V.I. Universal extended theories of integers. Algebra i Logika 16 (5), 588–602 (1977). (In Russian)
4. Lipshitz L. Some remarks on the Diophantine problem for addition and divisibility. Bull. Soc. Math. Belg. Ser. B 33, iss. 1, 41–52 (1981).
5. 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
6. Weispfenning V. The complexity of linear problems in fields. Journal of Symbolic Computation 5, iss. 1–2, 3–27 (1988). https://doi.org/10.1016/S0747-7171(88)80003-8
7. Gu´epin F., Haase C., Worrell J. On the existential theories of B¨uchi arithmetic and linear p-adic fields. Proceedings of the 34th Annual ACM / IEEE Symposium on Logic in Computer Science (LICS), 1–10 (2019). https://doi.org/10.1109/LICS.2019.8785681
8. Schmid H. L., Mahler K. On the Chinese remainder theorem. Mathematische Nachrichten 18, 120–122 (1958).
Загрузки
Опубликован
26.09.2021
Как цитировать
Старчак, М. Р. (2021). Доказательство теоремы Бельтюкова-Липшица квазиэлиминацией кванторов. I. Определения и НОД-лемма. Вестник Санкт-Петербургского университета. Математика. Механика. Астрономия, 8(3), 455–466. https://doi.org/10.21638/spbu01.2021.307
Выпуск
Раздел
Математика
Лицензия
Статьи журнала «Вестник Санкт-Петербургского университета. Математика. Механика. Астрономия» находятся в открытом доступе и распространяются в соответствии с условиями Лицензионного Договора с Санкт-Петербургским государственным университетом, который бесплатно предоставляет авторам неограниченное распространение и самостоятельное архивирование.
