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