В математической логике язык действительных чисел первого порядка представляет собой набор всех правильно построенных предложений логики первого порядка , которые включают в себя универсальные и экзистенциальные кванторы и логические комбинации равенств и неравенств выражений над действительными переменными. Соответствующая теория первого порядка представляет собой набор предложений, которые на самом деле верны для действительных чисел. Существует несколько различных таких теорий, обладающих разной выразительной силой в зависимости от примитивных операций, которые разрешено использовать в выражении. Фундаментальный вопрос при изучении этих теорий заключается в том, разрешимы ли они : то есть существует ли алгоритм , который может принимать предложение в качестве входных данных и выдавать на выходе ответ «да» или «нет» на вопрос, является ли это предложение верно в теории.
Теория реальных замкнутых полей — это теория, в которой примитивными операциями являются умножение и сложение; это означает, что в этой теории единственными числами, которые можно определить, являются действительные алгебраические числа . Как доказал Тарский , эта теория разрешима; см. теорему Тарского-Зейденберга и исключение кванторов . Текущие реализации процедур принятия решений для теории реальных замкнутых полей часто основаны на исключении кванторов посредством цилиндрического алгебраического разложения .
Разрешимый алгоритм Тарского был реализован на электронных компьютерах в 1950-х годах. Время его выполнения слишком медленное, чтобы он мог достичь каких-либо интересных результатов. [1]
Задача Тарского о показательной функции касается распространения этой теории на другую примитивную операцию — показательную функцию . Вопрос о разрешимости этой теории остается открытым, но если гипотеза Шануэля верна, то из этого следует разрешимость этой теории. [2] [3] Напротив, расширение теории действительных замкнутых полей с помощью функции синуса неразрешимо, поскольку это позволяет кодировать неразрешимую теорию целых чисел (см. теорему Ричардсона ).
Тем не менее, можно справиться с неразрешимым случаем с помощью таких функций, как синус, используя алгоритмы, которые не обязательно всегда завершаются. В частности, можно разработать алгоритмы, которые должны завершаться только для устойчивых входных формул , то есть формул, выполнимость которых не меняется, если формула слегка изменена. [4] Альтернативно можно использовать чисто эвристические подходы. [5]