Разрешимость теорий иерархий согласованных со сложением функций тема диссертации и автореферата по ВАК РФ 01.01.06, кандидат физико-математических наук Снятков, Алексей Сергеевич

• Снятков, Алексей Сергеевич
• кандидат физико-математических наук
• 2012

Оглавление диссертации кандидат физико-математических наук Снятков, Алексей Сергеевич

Введение

Актуальность.

Обзор литературы.

Цели работы.

Методы исследования.

Положения, выиосимые на защиту, и научная новизна

Апробация

Публикации.

Структура работы.

1 Определения

1.1 Согласованные со сложением функции

1.2 Разрешимые теории и сложность разрешающих процедур

2 Свойства иерархий функций

2.1 Поведение функций

2.2 Термы ^

3 Теория 7>

3.1 Элиминация кванторов в теории 7/.

3.2 Разрешимость теории Т/.

3.3 Периодичность /1.

4 Время работы алгоритма

4.1 Верхняя оценка времени алгоритма.

4.2 Нижняя оценка времени задачи

Введение диссертации (часть автореферата) на тему «Разрешимость теорий иерархий согласованных со сложением функций»

Актуально сть

Исследование разрешимости арифметических теорий — одна из центральных задач математической логики. Этим вопросом стали заниматься примерно с середины двадцатых годов 20 века. В начале и середине тридцатых годов были получены знаменитые теоремы Гёделя о неполноте и результат Чёрча о неразрешимости. Эти результаты открыли перспективу изучения разрешимости и индуцировали массу иследований о разрешимости и неразрешимости различных математических теорий.

Основными методами доказательства разрешимости являются:

1. Эффективная элиминация кванторов — это алгоритмический процесс, порождающий по заданной логической формуле другую, эквивалентную ей формулу, свободную от вхождений кванторов. Элиминация кванторов далеко не всегда возможна, но когда это так, алгоритм элиминации кванторов приносит исключительную пользу для исследователя, так как вскрывает структуру теории и её моделей. При использовании метода элиминация кванторов часто требуется расширение сигнатуры, что показывает выразительную силу таких теорий.

Самыми известными теориями, разрешимость которых была доказана при помощи элиминации кванторов, являются аддитивная арифметика целых чисел (арифметика Пресбургера) и теория вещественно замкнутых полей (действительных чисел со сложением и умножением).

Также известны следующие теории, разрешимость которых установлена методом элиминации кванторов: теория рациональных чисел с порядком, теория алгебраически замкнутых полей, теория булевых алгебр.

2. Метод интерпретаций: если известно, что теория Т\ разрешима, а все отношения в теории интерпретируются в теории Т\, то теория То также разрешима.

Например, Тарским было показано, что геометрия разрешима, так как интерпретируется в действительные числа.

3. Метод использования свойств формальных языков: Теория является разрешимой, если все отношения в этой теории могут быть закодированными с помощью какого-нибудь алфавита, и получившийся класс языков обладает свойством разрешимости, а также свойствами замкнутости, относительно операций пересечения, дополнения и некоторых других.

Одно из направлений исследований — поиск разрешимых обогащений арифметики Пресбургера. Один из наиболее значительных результатов был получен А.Л.Семеновым. Он ввёл понятие функций, согласованных со сложением, и рассматривал расширение арифметики Пресбургера такой функцией, а также доказал, что такая теория является разрешимой. Кроме того, А.Л.Семёновым было введено понятие класса редких предикатов и доказано, что теория, полученная расширением арифметики Пресбургера такими предикатами, является разрешимой. Также было доказано, что теория, полученная расширением арифметики Пресбургера порядком и умножением на одно произвольное число, разрешима. Теория, полученная расширением арифметики Пресбургера поразрядными операциями, также разрешима.

Примерно с шестидесятых годов 20 века начались исследования вычислительной сложности разрешимых проблем. На сложность разрешения теории можно смотреть как на меру её выразительных возможностей. В настоящее время вопрос об эффективности алгоритмов также приобретает всё большее практическое значение в связи с расширением применения вычислительной техники. Для решения задач с помощью вычислительной техники необходимо, чтобы они были алгоритмически разрешимыми и допускали разрешение с использованием ограниченного числоа ресурсов, поэтому важной теоретической и практической проблемой является установление вычислительной сложности логических задач, разрешимость которых известна.

Работы Фишера, Мейера и Рабина показывают, что многие теории, хотя они и являются разрешимыми, с практитечкой точки зрения таковыми не являются, потому что любой разрешающий алгоритм требовал бы практически невозможного числа вычислительных шагов. Так для арифметики сложения натуральных чисел, разрешимость которой доказана Пресбур-гером, было показано, что для каждого разрешающего алгоритма АЬ существует предложение А размера п такое, что для АЬ требуется 22" вычислительных шагов для ответа на вопрос по поводу А. Также этими же авторами показано, что разрешающая процедура для теории вещественно замкнутых полей обладает сложностью по меньшей мере 2п. Было показано, что для арифметики Пресбургера существует разрешающий алгоритм, который работает 222 шагов. Из других известных результатов отметим, что для доказательства разрешимости слабой монадической теории следования второго порядка, требуется не меньше гиперэкспоненты шагов.

Обзор литературы

В работах ряда авторов найдены неразрешимые проблемы и созданы общие методы доказательства неразрешимости теорий. Многие методы доказательства неразрешимости теорий изложены в известной монографии Тарского, Робинсона и Мостовского [45]. Первые неразрешимые теории были найдены Черчем (см. [29], [30], [2]), который доказал неразрешимость узкого исчисления предикатов, и Россером (см. [42]), который доказал неразрешимость арифметики натуральных чисел. После доказательства неразрешимости формальной арифметики появилось множество результатов, касающихся разрешимости различных математических теорий.

Разрешимость многих теорий была доказана с помощью метода элиминации кванторов. В 1929 году М.Пресбургер показал, что арифметика натуральных чисел с одним сложением разрешима (см. [2], [37]). Ряд классических результатов о разрешимости получены Тарским: теория вещественно замкнутых полей разрешима (см. [4], [44]), евклидова геометрия разрешима (см. [44]), теория булевых алгебр разрешима (см. [43]). Более простое доказательство последнего найдено Ершовым (см. [7], [8]). Аксом и Коченом (см. [23], [24], [25]) было доказано, что теория поля р-адических чисел разрешима. Также Аксом было доказано, что теория класса всех конечных полей разрешима. Эренфойхт в [32] показал, что теория линейно упорядоченных множеств разрешима. Первое полное доказательство этого результата было опубликовано Лёйхли и Леонардом в [36]. Позже этот результат стал простым следствием метода статьи Рабина (см. [41]). В [1] описаны результаты, посвящённые вопросу разрешимости и неразрешимости теорий, принадлежащие отечественным математикам.

В работах [13] и [14] А.Л.Семёновым были рассмотрены расширения арифметики Пресбургера функциями, согласованными со сложением и редкими предикатами. А.Л.Семёнов доказал, что оба варианта обогащения являются разрешимыми. В работе [12] И.В.Поповым было введено понятие периодичных по любому модулю, неубывающих функций, было рассмотрено расширение арифметики Пресбургера такой функцией, и показано, что такая теория является разрешимой. В работе [6] Дудаковым С.М. было рассмотрено одновременное обогащение арифметики Пресбургера одноместными функциональными и еще более редкими одноместными предикатными символами, и показано, что такая теория допускает элиминацию кванторов. В работе [10] Ю. Г. Пеизин доказал, что теория, полученная расширением арифметики Пресбургера порядком и умножением на одно произвольное число, разрешима. В [38] доказано, что если гипотеза Шануэля (см. [35]) для действительных чисел верна, то теория поля действительных чисел с экспонентой является разрешимой.

Одним из способов доказательства разрешимости теорий является метод использования свойств формальных языков. В статье [28] рассматриваются конечные автоматы для доказательства разрешимости теорий, вводится понятие автоматной системы. В [28] также доказано, что если система является автоматной, то по любой формуле этой системы можно эффективно построить конечный автомат, который проверяет её истинность, то есть теория такой системы является разрешимой. Например, системы (и;,+), ш, <), (¿2, <) (см. [3]) являются автоматными. В свою очередь, система (<0>,+) (см. [46]) не является автоматной, хотя ее теория допускает элиминацию кванторов и разрешима. В статье [И] понятие конечного автомата дополнятся рекурсивным оракулом и с помощью такой структуры доказывается разрешимость некоторых теорий автоматных систем, обогащенных одноместным предикатом вида С/ С {2х : х 6 ш}. Также в [11] приводится пример неавтоматной системы, теория которой не допускает элиминацию кванторов в исходной сигнатуре, но которая разрешима.

Значительное число работ посвящено исследованию вычислительной сложности. М. Блюмом в [27] дано формальное понятие аксиоматической меры сложности. При изучении сложности алгоритма нужно остановиться на каком-нибудь определённом уточнении понятия алгоритма. В качестве разрешающих процедур обычно выбирают алгоритмы, представленные в виде машины Тьюринга (см. [34]). В [21] показано, что все известные естественные формализации алгоритма по сложности эквивалентны машине Тьюринга (с точностью до полинома). Рабином в [40] была доказана теорема о сложности, а Блюмом в [27] — теорема об ускорении. Фишер и Ра-бин (см. [33]) нашли достаточные условия для доказательства трудности задач разрешения теорий в различных классах сложности. В частности, ими показано, что разрешающая процедура для арифметики Пресбургера обладает сложностью по меньшей мере 22". Там же установлено, что разрешающая процедура для теории вещественно замкнутых полей обладает сложностью по меньшей мере 2п. Однако, эту оценку точной назвать пока нельзя: Оппенен показал (см. [31]), что для арифметики Пресбургера существует разрешающий алгоритм, который работает 2" шагов и вопрос о том какая оценка точнее пока открыт. Мейер в [39] показал, что для доказательства разрешимости слабой монадической теории следования второго порядка требуется не меньше шагов.

0(п) раз

Цели работы

Данная работа посвящена исследованию свойств теорий

Т/ = ТЬ(а;, 0,1, <, 4-, /о, /ь - • •, /«), образованных из арифметики А.Л.Семенова +, /о) добавлением функций > 0, которые в работе названы «гиперфункциями». Каждая из них получается итерацией предыдущей. В частности, показано, что такие теории при определённых условиях являются разрешимыми. Также в работе изучается сложность разрешающей процедуры для таких теорий.

Методы исследования

Работа носит теоретический характер. В пей используются методы математической логики, теории алгоритмов и теории сложности. В работе усовершенствован метод элиминации кванторов А.Л. Семёнова. Для поиска нижней границы времени работы разрешающий процедуры был разработан метод кодирования последовательности с помощью бинарного дерева.

Положения, выносимые на защиту, и научная новизна

Все полученные результаты являются новыми. На защиту выносятся следующие основные результаты.

1. Доказано, что если все функции являются периодичными по любому натуральному модулю, то любая формула в теориях Т/ эквивалентна экзистенциальной. Следовательно эти теории являются модельно полными. Показано, что преобразование каждой формулы к экзистенциальной может быть эффективным, если все гиперфункции являются эффективно периодичными по любому натуральному модулю. Установлено, что если обогатить теорию обратными для /г функциями, то получается теория с элиминацией кванторов. Элиминация будет эффективной при упомянутом выше условии. Таким образом, при выполнении условия эффективной периодичности гиперфункций, теории являются разрешимыми.

2. Установлено, что если функция /о — периодичная по любому модулю р > 1с периодом меньше р, то гиперфункция от /о является эффективно периодичной по любому модулю р > 1 с периодом 1. Также установлено, что если функция /о — периодичная по любому модулю р > 1с периодом меньше р, а функция fi(x) — периодичная функция, то гиперфункция от функции f(x) fi(x) является периодичной по модулю р для любого р > 1. Следовательно, теории, для которых выполняется одно из двух условий, являются разрешимыми.

3. Показано, что представленный в работе разрешающий алгоритм для любой формулы длины п для определения её истинности в Т/ требует па

2 п мяти не больше чем • Следовательно, разрешающий алгоритм ра

0(п) раз 2" ботает не более ^^ шагов.

0{п) раз

4. Предложен метод кодирования последовательности с помощью бинарного дерева. Используя этот метод, доказано, что для любого разрешающего алгоритма существует формула длины п, для которой время работы алгоритма, определяющего истиность формулы в Т/, будет не меньше 2 чем ,2^, . Таким образом, задача разрешения указанных теорий являем (п) раз ется полной в классе сложности TIME | ) •

Ю(п) раз

Апробация

Начиная с 2006 года содержание глав данной диссертации неоднократно докладывалось на семинаре «Теоретические основы информатики» в ТвГУ.

Доклад по теме диссертации был сделан в 2008 году в Санкт-Петербургском отделении Математического института им.В.А.Стеклова РАН на семинаре по математической логике под руководством академика РАН Ю.В.Матиясевича.

Также доклад по теме диссертации был сделан в 2011 году на международной конференции «Актуальные проблемы прикладной математики, информатики и механики» (Воронеж).

Исследования по теме работы были поддержаны РФФИ, проект № 08-01-00241-а.

Публикации

Список публикаций по теме диссертации включает 5 работ [15], [16], [17], [18], [19]. Работы [16], [17], [19] опубликованы в изданиях, входящих в список рекомендованных ВАК ведущих рецензируемых изданий.

Структура работы

Работа состоит из титульного листа, оглавления, четырех глав основной части, заключения и списка литературы.

В параграфе 1 мы даем основные определения, которые используются в диссертации. В 1.1 приводятся определения согласованной со сложением функции и иерархии таких функций. В 1.2 приводятся определения разрешимых теорий и определения, касающиеся вычислительной сложности алгоритмов.

В параграфе 2.1 мы устанавливаем основные свойства иерархии функций, согласованных со сложением. Показываем, что любая функция из иерархии либо строго возрастает, либо является константой, начиная с некоторого аргумента. Также мы демонстрируем, что любая функция из иерархии растет не медленнее, чем предыдущая.

В параграфе 2.2 мы определяем термы, с которыми будем в дальнейшем работать:

Ыу, а*, сц+1,., а,) = /г(/ш(- • • (/.ы(/> + + а^-х).) + ат) + аг), где г ^ у, все а^ — константы, после чего, доказываем для них ряд важных для нас свойств.

В параграфе 3.1 мы даем определение теории, образованной из арифметики А.Л.Семенова добавлением функций /¿,г > 0, полученных итерацией согласованной со сложением функции /о, которую мы называем Ту. После чего мы доказываем, что если все гиперфункции являются периодичными по любому натуральному модулю, то любая формула в этой теории эквивалентна экзистенциальной. Далее показано, что преобразование каждой формулы к экзистенциальной может быть эффективным при условии, что все гиперфункции являются эффективно периодичными по любому натуральному модулю.

В параграфе 3.2 мы демонстрируется, что если обогатить систему тории обратными функциями для /¿, то получается система с элиминацией кванторов, которая также может быть эффективной при упомянутом выше условии. Таким образом мы показываем, что при выполнении условия эффективной периодичности гиперфункций теории являются разрешимыми.

В параграфе 3.3 мы доказываем теоремы, в которых находятся условия на функцию /о, при которых функции /г- будут эффективно периодичными по любому натуральному модулю.

В параграфе 4.1 мы доказываем ряд лемм, при помощи которых оцениваем константы, используемые в разрешающем алгоритме, который приведён в параграфе 3.2. Затем показываем, что время работы разрешающего о.2" алгоритма для любой формулы из теории Т/ не больше, чем , если

0(п) раз формула была длиной п.

В параграфе 4.2 продемонстрирован метод кодирования последовательности с помощью бинарного дерева. Используя этот метод, доказано, что для любого разрешающего алгоритма существует формула длины п из тео2 рии Т/, для которой время работы алгоритма будет не меньше чем •

О(п) раз

В заключении ещё раз перечисляются полученные результаты и формулируются открытые вопросы, которые могут служить направлением дальнейших исследований.

Список литературы состоит из 46 наименований.

Заключение диссертации по теме «Математическая логика, алгебра и теория чисел», Снятков, Алексей Сергеевич

Заключение

В диссертации получены следующие основные результаты:

1. Если все гиперфункции являются периодичными по любому натуральному модулю, то любая формула в теории эквивалентна экзистенциальной.

2. Преобразование каждой формулы к экзистенциальной является эффективным при условии, что все функции /г- являются эффективно периодичными по любому натуральному модулю.

3. Если обогатить систему теории Ту обратными функциями для /;, то получится система с элиминацией кванторов, которая также может быть эффективной при упомянутом выше условии.

4. При выполнении условия эффективной периодичности гиперфункций теории являются разрешимыми.

5. Если функция /о — периодичная по любому модулю р > 1с периодом меньше р, то гиперфункция от /о является эффективно периодичной по модулю р > 1с периодом 1.

6. Если функция /о — периодичная по любому модулю р > 1 с периодом меньше р, а функция /1(2) — периодичная функция, тогда гиперфункция от функции /(ж) + является периодичной по модулю р, для любого р > 1.

7. Теория системы ТЬ(о;, 0,1, <, +, /о, /1,. • /т) требует для разрешения не больше чем 2~ времени.

Г/ = ТЬ(а;,0,1)<,+|/о,/ь.>/п)

0{п) раз

8. Теория системы Th(w, 0,1, <, +, /о, /1,. /т), если в ней существует формула, которая взаимно однозначно кодирует два натуральных числа, о.2 требует для разрешения не меньше чем ' гДе # — некоторая кон

0(п) раз станта. Таким образом задача разрешения указанных теорий является полной в классе сложности TIME ( ,2^, J.

Ю(п) раз

Дальнейшие иследования в данной области могут в себя включать:

1. Расширения класса функций согласованных со сложением, для которых гиперфункции будут периодичными по любому модулю.

2. Исследования теорий, полученных из арифметики Пресбургера, добавлением функции Аккермана, при фиксировании второго аргумента.

Мы хотим выразить благодарность участникам семинара по математической логике ПОМИ РАН и лично академику Ю.В.Матиясевичу, участникам семинара «Теоретические основы информатики» в ТвГУ за ценные советы и замечания.

Список литературы диссертационного исследования кандидат физико-математических наук Снятков, Алексей Сергеевич, 2012 год

1. Адян С.И. Алгоритмические проблемы для групп и полугрупп /С.И. Адян, В.Г. Дурнев//УМЫ. - 2000. - 55:2(332). - С. 3-94.

2. Булос Дж. Вычислимость и логика/Дж. Булос, Р.Джеффри. М.: Мир, 1994. - 396 с.

3. Васылкина Л.В. Структура ((¿,<) является автоматной/Л.В. Васыл-кина//Вестник ТвГУ. Серия: Прикладная математика. 2006. - № 3. - С. 42-45.

4. Верещагин Н.К. Языки и исчисления/Н.К. Верещагин, А. Шепь. М.: МЦНМО, 2002. - 291 с.

5. Гери М. Вычислительные машины и труднорешаемые задачи/М. Гери, Д. Джонсон. М.: Мир, 1982. - 416 с.

6. Дудаков С.М. Трансляционная теорема и автоматные структуры/С.М. Дудаков// Вестник ТвГУ. Серия Прикл. матем. 2006. - 4(21). - С. 5-35.

7. Ершов Ю.Л. Разрешимость элементарной теории дистрибутивных структур с относительными дополнениями и теории фильтров/Ю.Л. Ершов//Алгебра и логика. 1964. - № 3, С. 17-38

8. Ершов Ю.Л. Проблемы разрешимочти и конструктивные моде-ли/Ю.Л. Ершов. М.: Наука, 1980. - 415 с

9. Кейслер Г. Теория моделей /Г. Кейслер, Ч. Чен. М.: Мир, 1977. - 614 с.

10. Пензин Ю. Г. Разрешимость теории целых чисел со сложением, порядком и умножением на произвольное число/Ю. Г. Пензин//Матем. заметки. 1973. - 13:5. - С. 667-675

11. Петров А.Е. Разрешимость теорий обобщений автоматных систем/А.Е. Петров// Вестник ТвГУ. Сер. Прикл. матем. 2010. - №17. С. 21-40

12. Попов И.В. Элиминация кванторов в некоторых обогащениях арифметики Пресбургера/И.В. Попов// Сложные системы: обработка информации, моделирование и оптимизация, Тверь. 2002. - С. 38-47.

13. Семёнов A.JI. Логические теории одноместных функций на натуральном ряде/A.JI. Семёнов//Изв. АН СССР. 1983. - 47(3). - С. 623-658.

14. Семёнов А.Л. О некоторых расширениях арифметики сложения натуральных чисел/А.Л. Семёнов//Изв. АН СССР. 1979. - 43(5). - С. 1175-1195.

15. Снятков A.C. Разрешимость теории Тс = Th(a;, 0,1, <, 4-, СХ)/А.С. Снятков// Вестник ТвГУ. Сер. Прикл. матем. 2007. - 5(35). - С. 113-121

16. Снятков A.C. Разрешимость теории Tj — Th(w,0,1, < , +, f(x), F(x))/A.C. Снятков// Вестник ТвГУ. Сер. Прикл. матем. 2008. - 14(34). - С. 67-77

17. Снятков A.C. Разрешимость теории Tf = Th(a;, 0,1, < 5 +> f(x),., fn)/A.C. Снятков// Модел. и анализ информ. систем. -2010. 17:3. - С. 72-90

18. Снятков A.C. Разрешимость теории Tf — Th(o;,0,1,< , +, f{x),., fn)./A.C. Снятков//Актуальные проблемы прикладной математики, информатики и механики. Сборник трудов международной конференции. 2011. - С. 362-365.

19. Снятков A.C. Нижняя граница времени для разрешения теории с функцией экспоненты/А.С. Снятков// Вестник ТвГУ. Сер. Прикл. матем. 2012. - №17. - Выпуск 2 (25). - С. 5-10.

20. Столбоушкин А.П. Математические основы информатики/А.П. Стол-боушкин, М.А. Тайцлин

21. Трахтенброт Б.А. Сложность алгоритмов и вычислений/Б.А. Трах-тенброт. Новосибирск: изд-во НГУ, 1967. - 247 с.

22. Ackermann W. Zum Hilbertschen Aufbau der reellen Zahlen/W. Ackermann// Mathematische Annalen. 1928. - 99. P. 118-133.

23. Ax J. Diophantine problems over local fields, I/J. Ax, S. Kochen//Amer. J. Math. 1965. - 87. - P. 605-630.

24. Ax J. Diophantine problems over local fields, II. A complete set of axioms for p-adic number theory/J. Ax, S. Kochen//Amer. J. Math.- 1965. 87. - P. 631-648.

25. Ax J. Diophantine problems over local fields, III. Decidable fields/J. Ax, S. Kochen//Ann. Math. 1966. - 83. - P. 437-456

26. Ax J. The elementary theory of finite fields/J. Ax//Ann. Math. 1968. -88. - P. 239-271.

27. Blum M. A Machine-Independent Theory of the Complexity of Recursive Functions/M. Blum//Journal of the ACM. 1967. - 14 (2). - P. 322-336.

28. Blumensath A. Automatic structures/A. Blumensath, E.Graedel//Proc. 15th IEEE Symp. on Logic in Computer Science-Cambridge, 2000. P. 51-62.

29. Church A. A note on the Entscheidungs problem/A. Church//Journal of Symbolic Logic. 1936. - № 1. - P. 40-41

30. Church A. An unsolvable problem of elementary number theory/A. Church//Amer. Journ. of Math. 1936. - 58. - P. 345-363.

31. Oppen D. C. A 22 Upper Bound on the Complexity of Presburger Arithmetic/D. C. Oppen//J. Comput. Syst. Sei. 1978. - 16(3). - P. 323332

32. Ehrenfeucht A. Decidability of the theory of linear ordering relation. -Notices Amer. Math. Soc., 1959, 6, P. 268-269

33. Fischer. M. J. Super-Exponential Complexity of Presburger Arithmetic/M. J. Fischer, M.O. Rabin//Proceedings of the SIAM-AMS Symposium in Applied Mathematics Vol. 7. New York, 1974. - P. 27-41.

34. Garey M.R. Computers and Intractability. A Guide to the Theory of NP-Completeness/M.R. Garey, D.S. Johnson. San Francisco, W.H.Freeman and Company, 1979,- 338 p.

35. Lang S. Introduction to Transcendental Numbers/S. Lang//Addison-Wesley. 1966. - P. 30-31.

36. Lauchli H. On the elementary theory of linear order/H. Lauchli, J. Leonard//Fundam. math. 1966. - 59. - P. 109-116.

37. Macintyre A.J. On the decidability of the real exponential field/A.J. Macintyre, A.J. Wilkie//Kreisel 70th Birthday Volume. 2005. - P. 441467.

38. Meyer A.R. The inherent complexity of theories of ordered sets/A.R. Meyer//Proceedings of the International Congress of Mathematics. -Vancouver, 1974. P. 477-482.

39. Rabin M. O. Speed of Computation of Functions and Classification of Recursive Sets/M. O. Rabin//Bull. Res. Council Israel 8F. 1959. - P. 69-70.

40. Rabin M. O. A simple method for undecidability proofs and some applications/M. O. Rabin//Logic, Methodology and Philosophy of Science, Ii/Ed. Y. Bar-Hillel. Amsterdam: North-Holland. 1969. - P. 92-101

41. Rosser J. B. Extensions of some theorems of Godel and Church/J. B. Rosser//JSL, 1. Chandler's Ford, 1936. - P. 87-91.

42. Tarski A. Arithmetical classes and types of Boolean algebras: Preliminary report/A. Tarski//Bull. Amer. Math. Sos. 1949. - 55. - 64 p.

43. Tarski A. A Decision Method for Elementary Algebra and Geometry/A. Tarski. Los Angeles, Berkeley, 1951. - 63 p.

44. Tarski A. Undecidable theory/A. Tarski,R. Robinson,A. Mostowski. -Amsterdam, North-Holland, 1953. 116 p.

45. Tsankov T. The additive group of the rationals does not have an automatic presentation/T. Tsankov// The Journal of Symbolic Logic.-2011.-76(4).-P. 1341-1351.