Разрешимость теорий действительных чисел первого порядка
 | Эта статья нуждается в дополнительных ссылок для проверки . ( сентябрь 2014 г. ) |
В математической логике язык действительных чисел первого порядка представляет собой набор всех правильно сформированных предложений логики первого порядка , которые включают в себя универсальные и экзистенциальные кванторы и логические комбинации равенств и неравенств выражений над действительными переменными. Соответствующая теория первого порядка представляет собой набор предложений, которые на самом деле верны для действительных чисел. Существует несколько различных таких теорий, обладающих разной выразительной силой в зависимости от примитивных операций, которые разрешено использовать в выражении. Фундаментальный вопрос при изучении этих теорий заключается в том, разрешимы ли они : то есть существует ли алгоритм , который может принимать предложение в качестве входных данных и выдавать на выходе ответ «да» или «нет» на вопрос, является ли это предложение верно в теории.
Теория реальных замкнутых полей — это теория, в которой примитивными операциями являются умножение и сложение; это означает, что в этой теории единственными числами, которые можно определить, являются действительные алгебраические числа . Как доказал Тарский , эта теория разрешима; см. теорему Тарского-Зейденберга и исключение кванторов . Текущие реализации процедур принятия решений для теории реальных замкнутых полей часто основаны на исключении кванторов посредством цилиндрического алгебраического разложения .
Разрешимый алгоритм Тарского был реализован на электронных компьютерах в 1950-х годах. Время его выполнения слишком медленное, чтобы он мог достичь каких-либо интересных результатов. [1]
Задача Тарского о показательной функции касается распространения этой теории на другую примитивную операцию — показательную функцию . Вопрос о разрешимости этой теории остается открытым, но если гипотеза Шануэля верна, то из этого следует разрешимость этой теории. [2] [3] Напротив, расширение теории действительных замкнутых полей с помощью функции синуса неразрешимо, поскольку это позволяет кодировать неразрешимую теорию целых чисел (см. теорему Ричардсона ).
Тем не менее, можно справиться с неразрешимым случаем с помощью таких функций, как синус, используя алгоритмы, которые не обязательно всегда завершаются. В частности, можно разработать алгоритмы, которые должны завершаться только для устойчивых входных формул , то есть формул, выполнимость которых не меняется, если формула слегка изменена. [4] Альтернативно также возможно использовать чисто эвристические подходы. [5]
См. также [ править ]
Ссылки [ править ]
- ^ А. Бурдман Фефферман и С. Фефферман, Альфред Тарский: жизнь и логика (Кембридж: Cambridge University Press, 2008).
- ^ Макинтайр, Эй Джей ; Уилки, AJ (1995), «О разрешимости реального экспоненциального поля», в Одифредди, PG (ред.), Том, посвященный 70-летию Крейзеля , CLSI
- ^ Кульманн, С. (2001) [1994], «Модельная теория действительной показательной функции» , Энциклопедия математики , EMS Press
- ^ Ратчан, Стефан (2006). «Эффективное решение количественных ограничений неравенства над действительными числами». Транзакции ACM в вычислительной логике . 7 (4): 723–748. arXiv : cs/0211016 . дои : 10.1145/1183278.1183282 . S2CID 16781766 .
- ^ Акбарпур, Бехзад; Полсон, Лоуренс Чарльз (2010). «МетиТарский: автоматическое средство доказательства теорем для специальных функций с действительным знаком». Журнал автоматизированного рассуждения . 44 (3): 175–205. дои : 10.1007/s10817-009-9149-2 . S2CID 16215962 .
 | Эта алгебраической геометрии статья, посвященная , незавершена . Вы можете помочь Википедии, расширив ее . |