В современном мире арифметика Пресбургера нашла применение не только в математике, но и во многих прикладных областях [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. Доказаны теоремы о неразрешимости некоторых расширений арифметики Семёнова.
