Алгоритм Тарского Реализация алгоритма Тарского для случая одной переменной Авторы: Ерохин С., Устинов Н., Климовицкий И., Смыкалов В., Тыщук К., Савенков К., Явейн А. Руководитель: Бреслав А. А. ФМЛ 239, 10-1

Постановка задачи: Реализация алгоритма Тарского для одной переменной: выяснить верно ли выражение.

Структурные части алгоритма: преобразование вводимой формулы в дерево лексер парсер арифметика длинных чисел натуральных рациональных арифметика полиномов дополнение данной системы полиномов до насыщенной системы построение таблицы знаков полиномов проверка истинности формулы построение графиков исходных многочленов

Парсер Синтаксис входного языка: натуральные числа: рациональные числа: -2 67/8 -3/4 переменные: x _67h f_7y знаки: + - * \ ^ знаки неравенства: > = логические связки: and or --> not(!) кванторы: E A Пример формулы: E x { [x^3*5/(4 + 1) > 5*x] and [[2 [x^7 - 1/3 = 2]] }

Преобразование данных [23 > 0] [2 < x][not [23 > 0]] or [2 < x] x 2 /5 + (-7*x + 6)*2 0

Дерево: корневая вершина: квантор внутренняя вершина: and, or или not лист: неравенство Неравенство: знак полином Полином – массив рациональных коэффициентов при степени x, в i-той ячейке коэффициент при x i. Рациональное число – знак и два натуральных числа - числитель и знаменатель. Натуральное число – динамический массив чисел типа Word. Представление данных

Пример дерева E x or not -3*x 3 – 7/5*x > 0 65 = 0 E x {[-7/5*x > 3*x^3] --> [(x - 5)*x = x^2 – 5*x - 65]}

Алгоритм входные данные извлечение полиномов построение насыщенной системы проверка истинности формулы построение таблицы знаков

Построение насыщенной системы Упорядочивание полиномов Будем считать полином f больше полинома g (записывается: f > g), если: степень f больше степени g; в случае равенства степеней разность f - g имеет положительный старший коэффициент Построение насыщенной системы происходит индуктивно, от старших степеней к младшим. На всех этапах построения множество полиномов отсортировано по возрастанию.

Построение насыщенной системы Получение полиномов k-ой степени: дифференцирование полиномов k+1 степени; деление с остатком всех полиномов k+1 степени и выше на полиномы k+1 степени Исключаются дубликаты и константы.... xkxk x k+1... x k+1 x k+2...

Построение таблицы знаков Заполняется последовательно, по строчкам. При добавлении нового столбца, столбец полностью заполняется. x1x1... …… … xkxk +0- … заполняем

Проверка истинности формулы x *x x2-9x При кванторе существования поиск подходящего столбца. При кванторе всеобщности поиск неподходящего столбца. не верно верно

?