В современном мире арифметика Пресбургера нашла применение не только в математике, но и во многих прикладных областях [6]. Арифметика Пресбургера представляет собой элементарную теорию целых чисел с нулём, единицей, сложением и отношением порядка.
Уже долгое время ведутся исследования как самой арифметики, так и вопросов, связанных с различными ее расширениями. Большая часть исследований была посвящена проблемам сложности и разрешимости этой теории, а в дальнейшем и различных расширений этой теории. Ва- риациии алгоритма Д.Купера [4] дают эффективные на практике алгоритмы элиминации кванторов для этой теории. Позже В.Вайспфеннинг [17] предложил эффективные методы элиминации кванторов для арифметики вещественных чисел со сложением и отношением порядка.
Следуя А.Семёнову и С.Сопрунову [22], определим структуру сигнатуры а как тройку (D; а, Int). Здесь D - это множество (в данной работе это будут множества N, Z, R), называемое универсумом (или областью) структуры, Int - это интерпретация, которая каждое n-местное имя отношения из а отображает в n-арное отношение на D, другими словами — в подмножество Dn, а каждое n-местное имя функции — в функцию из Dn в D. Так как в дальнейшем интерпретация Int будет обычно ясна из контекста, будем записывать просто (D; а).
Алгоритм элиминации кванторов для некоторой структуры можно опредеделить следующим образом. Рассмотрим язык первого порядка La некоторой сигнатуры а, и пусть задана некоторая структура (D; а) сигнатуры а. Алгоритм элиминации кванторов для (D; а) - это такой конечный алгоритм, который для любой формулы ф языка La предоставляет бескванторную формулу ф' этого же языка, такую что формулы ф и ф' эквивалентны в структуре (D; а) и формула ф' не содержит связанных переменных.
Есть большое количество результатов, в которых доказывается и явно приводится алгоритм элиминации кванторов для различных структур. Множество из этих алгоритмов реализовано в системе Redlog [5].
Разработка Redlog [5] была начата в 1992 году А. Дольцманом и
Т.Штурмом. Данная система является расширением системы компьютерной алгебры REDUCE [13] и содержит в себе множество эффективных алгоритмов элиминации кванторов для различных теорий. Система REDUCE нашла широкое применение в научных вычислениях, физике, инженерных науках и других областях.
Важной задачей является нахождение достаточно выразительных структур (в частности, расширений арифметики Пресбургера), для которых существует алгоритм элиминации кванторов. Такие алгоритмы затем могут быть внедрены в систему RedLog для отдельных классов формул, для которых применение элиминации кванторов оказывается достаточно эффективным. Очевидно, что чем более выразителен язык, тем труднее с вычислительной точки зрения окажется алгоритм, и тем чаще в случае произвольных формул соответствующей сигнатуры мы будем сталкиваться с алгоритмичсеки неразрешимыми проблемами. Такого рода чисто теоретические вопросы представляют неменьший интерес.
В ходе выполнения работы были выполнены следующие задачи:
1. Исследованы известные алгоритмы и подходы для элиминации кванторов
2. Исследован явный алгоритм элиминации кванторов для структуры (N, +, 2х}.
3. Доказаны теоремы о неразрешимости некоторых расширений арифметики Семёнова.
