 | Эта статья требует дополнительных ссылок для проверки . ( сентябрь 2014 г. ) ( Узнайте, как и когда удалить это сообщение-шаблон ) |
В математической логике , язык первого порядка из действительных чисел является множеством всех хорошо сформированных предложений по логике первого порядка , которые включают универсальные и экзистенциальные кванторы и логические комбинации равенств и неравенства выражений над вещественными переменными. Соответствующая теория первого порядка - это набор предложений, которые действительно верны для действительных чисел. Существует несколько различных таких теорий с разной выразительной силой в зависимости от примитивных операций, которые разрешено использовать в выражении. Фундаментальный вопрос при изучении этих теорий - разрешимы ли они?: то есть, существует ли алгоритм, который может принимать предложение в качестве входных данных и выдавать в качестве выходных данных ответ «да» или «нет» на вопрос о том, истинно ли предложение в теории.
Теория реальных замкнутых полей - это теория, в которой примитивными операциями являются умножение и сложение; это означает, что в этой теории можно определить только действительные алгебраические числа . Как доказал Тарский , эта теория разрешима; см. теорему Тарского – Зайденберга и исключение кванторов . Современные реализации процедур принятия решений для теории реальных замкнутых полей часто основаны на исключении кванторов с помощью цилиндрической алгебраической декомпозиции .
Проблема экспоненциальной функции Тарского касается расширения этой теории до другой примитивной операции - экспоненциальной функции . Вопрос о разрешимости этой теории остается открытым, но если гипотеза Шенуэля верна, то разрешимость этой теории будет следовать. [1] [2] Напротив, расширение теории вещественных замкнутых полей с помощью синус-функции неразрешимо, поскольку это позволяет кодировать неразрешимую теорию целых чисел (см . Теорему Ричардсона ).
Тем не менее, можно справиться с неразрешимым случаем с помощью таких функций, как синус, используя алгоритмы, которые не обязательно завершаются всегда. В частности, можно разработать алгоритмы, которые требуются только для завершения только для устойчивых входных формул , то есть формул, выполнимость которых не меняется, если формула слегка нарушена. [3] В качестве альтернативы также можно использовать чисто эвристические подходы. [4]
Ссылки [ править ]
- ^ Macintyre, AJ ; Уилки, AJ (1995), "О разрешимости действительного экспоненциального поля", в Odifreddi, PG (ed.), Kreisel 70th Birthday Volume , CLSI CS1 maint: обескураженный параметр ( ссылка )
- ^ Kuhlmann, S. (2001) [1994], "Модельная теория действительной экспоненциальной функции" , Энциклопедия математики , EMS Press
- ^ Ratschan, Стефан (2006). «Эффективное решение количественных ограничений неравенства над действительными числами». ACM-транзакции по вычислительной логике . 7 (4).
- ^ Акбарпур, Бехзад; Полсон, Лоуренс Чарльз (2010). "МетиТарский: автоматическое средство доказательства теорем для вещественнозначных специальных функций". Журнал автоматизированных рассуждений . 44 . CS1 maint: обескураженный параметр ( ссылка )
