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

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