Разрешимость теорий действительных чисел первого порядка

• Язык вещественных чисел первого порядка — набор правильно сформированных предложений логики первого порядка с кванторами и равенствами/неравенствами над вещественными переменными. 
• Теория первого порядка — набор предложений, истинных для действительных чисел. 
• Существуют различные теории первого порядка с разной выразительной силой. 
• Теория реальных замкнутых полей разрешима, так как примитивными операциями являются умножение и сложение. 
• Современные реализации процедур принятия решений основаны на исключении квантификатора через цилиндрическую алгебраическую декомпозицию. 
• Задача Тарского об экспоненциальной функции остается открытой, но если гипотеза Шануэля верна, то теория разрешима. 
• Расширение теории реальных замкнутых полей с синусоидальной функцией неразрешимо из-за возможности кодирования неразрешимой теории целых чисел. 
• Неразрешимые случаи можно решить с помощью алгоритмов, требующих завершения работы с устойчивыми формулами или эвристических подходов.