Войти
В математике и информатике Entscheidungsproblem (произносится, немецкий для «проблемы решения») - это вызов, поставленный Дэвидом Гильбертом и Вильгельмом Аккерманом в 1928. Задача запрашивает алгоритм , который рассматривает в качестве входных данных утверждение и отвечает «Да» или «Нет» в зависимости от того, является ли утверждение универсальным, т. Е. Действительным в каждой структуре удовлетворяющие аксиомам.
Согласно теореме полноты логики первого порядка, утверждение универсально справедливо тогда и только тогда, когда оно может быть выведено из аксиом, так что Entscheidungsproblem также можно рассматривать как запрос алгоритма, чтобы решить, доказуемо ли данное утверждение на основе аксиом с использованием правил логики.
В 1936 году Алонзо Черч и Алан Тьюринг опубликовали независимые статьи, показывающие, что общее решение проблемы Entscheidungsproblem невозможно, если предположить, что интуитивное понятие «эффективно вычислимое » улавливается функциями, вычисляемыми с помощью машины Тьюринга (или эквивалентно, выражаемыми в лямбда-исчислении ). Это предположение теперь известно как тезис Черча-Тьюринга.
Происхождение проблемы Entscheidungs восходит к Готфриду Лейбницу, который в семнадцатом веке, после создания успешной механической вычислительной машины, мечтал о создании машины, которая могла бы манипулировать символами для определения значений истинности математических утверждений. Он понял, что первым шагом должен быть чистый формальный язык, и большая часть его последующей работы была направлена на достижение этой цели. В 1928 г. Давид Гильберт и Вильгельм Аккерман поставили вопрос в изложенной выше форме.
В продолжение своей «программы» Гильберт задал три вопроса на международной конференции в 1928 году, третий из которых стал известен как «Entscheidungsproblem Гильберта». В 1929 году Моисей Шенфинкель опубликовал одну статью об особых случаях проблемы принятия решений, которую подготовил Пол Бернейс.
. Еще в 1930 году Гильберт считал, что не будет такой вещи, как неразрешимая проблема.
Прежде чем можно было ответить на вопрос, нужно было формально определить понятие «алгоритм». Это было сделано Алонзо Черч в 1935 году с концепцией «эффективной вычислимости», основанной на его λ-исчислении, и Аланом Тьюрингом в следующем году с его концепцией машин Тьюринга.. Тьюринг сразу же признал, что это эквивалентные модели вычислений.
Отрицательный ответ на Entscheidungsproblem был дан Алонзо Чёрчем в 1935–1936 гг. (теорема Чёрча ) и независимо вскоре после этого Алан Тьюринг в 1936 г. (доказательство Тьюринга ). Черч доказал, что не существует вычислимой функции, которая решает для двух заданных выражений λ-исчисления, эквивалентны они или нет. Он в значительной степени полагался на более ранние работы Стивена Клини. Тьюринг свел вопрос о существовании «общего метода», который решает, останавливается ли данная машина Тьюринга или нет (проблема остановки ), к вопросу о существовании «алгоритма» или «общего метода». смог решить проблему Entscheidungsproblem. Если «алгоритм» понимается как эквивалент машины Тьюринга и с отрицательным ответом на последний вопрос (в общем), вопрос о существовании алгоритма для Entscheidungsproblem также должен быть отрицательным (в общем). В своей статье 1936 года Тьюринг говорит: «В соответствии с каждой вычислительной машиной« оно »мы строим формулу« Un (it) »и показываем, что, если существует общий метод определения доказуемости« Un (it) », то есть общий метод определения того, выводит ли "оно" когда-либо 0 ".
На работу Чёрча и Тьюринга сильно повлияла более ранняя работа Курта Гёделя над его теоремой о неполноте, особенно методом присваивания чисел (a гёделевская нумерация ) до логических формул, чтобы свести логику к арифметике.
Entscheidungsproblem связана с десятой проблемой Гильберта, которая требует алгоритма, чтобы решить, есть ли у диофантовых уравнений решение. Отсутствие такого алгоритма, установленного Юрием Матиясевичем в 1970 году, также подразумевает отрицательный ответ на проблему Entscheidungs.
Некоторые теории первого порядка разрешимы алгоритмически; Примеры этого включают арифметику Пресбургера, реальные закрытые поля и системы статических типов многих языков программирования. Однако общая теория первого порядка натуральных чисел, выраженная в аксиомах Пеано, не может быть решена с помощью алгоритма.
Наличие практических процедур принятия решений для классов логических формул представляет значительный интерес для верификации программ и верификации схем. Чистые булевы логические формулы обычно решаются с использованием методов SAT-решения, основанных на алгоритме DPLL. Конъюнктивные формулы над линейной действительной или рациональной арифметикой могут быть решены с использованием симплексного алгоритма, формулы в линейной целочисленной арифметике (арифметика Пресбургера ) могут быть решены с использованием или Уильям Пью с. Формулы с отрицаниями, союзами и дизъюнкциями сочетают в себе трудности проверки выполнимости с трудностями определения союзов; в настоящее время они обычно решаются с использованием методов SMT-решения, которые сочетают SAT-решение с процедурами принятия решения для соединений и методов распространения. Действительная полиномиальная арифметика, также известная как теория вещественных замкнутых полей, разрешима; это теорема Тарского – Зайденберга, которая была реализована на компьютерах с помощью цилиндрического алгебраического разложения.
Словарь определения entscheidungsproblem в Викисловаре