Проблема разрешения (нем. Entscheidungsproblem) кратко

Привет, Вы узнаете о том , что такое проблема разрешения , Разберем основные их виды и особенности использования. Еще будет много подробных примеров и описаний. Для того чтобы лучше понимать что такое проблема разрешения , entscheidungsproblem , настоятельно рекомендую прочитать все из категории Языки и методы программирования. Теория трансляции.

проблема разрешения (нем. Entscheidungsproblem) — задача из области оснований математики, сформулированная Давидом Гильбертом в 1928 году: найти алгоритм, который бы принимал в качестве входных данных описание любой проблемы разрешимости (формального языка и математического утверждения « » на этом языке) — и, после конечного числа шагов, останавливался бы и выдавал один из двух ответов: «Истина!» или «Ложь!», — в зависимости от того, истинно или ложно утверждение « ». Ответ не требует обоснований, но должен быть верным.

Такой алгоритм мог бы, к примеру, подтвердить гипотезу Гольдбаха и гипотезу Римана несмотря на то, что доказательства (и опровержения) пока неизвестны. Нерешаемость проблемы разрешения (неразрешимость множества истинных формул арифметики) для языка арифметики, содержащего «равенство», «сложение» и «умножение», является следствием неарифметичности этого множества. Неарифметичность является следствием теоремы Тарского «о невыразимости понятия истинности в языке средствами того же языка»

В 1936 году — Алонзо Черч и независимо от него Алан Тьюринг опубликовали работы, в которых показали, что не существует алгоритма для определения истинности утверждений арифметики, а поэтому и более общая проблема разрешения также не имеет решения. Этот результат получил название: «теорема Черча — Тьюринга».

Теорема о полноте

Согласно теореме о полноте логики первого порядка , утверждение является универсально действительным тогда и только тогда, когда оно может быть выведено из аксиом, поэтому проблему Entscheidungsproblem можно также рассматривать как требование алгоритма решить, доказуемо ли данное утверждение на основе аксиом. Об этом говорит сайт https://intellect.icu . используя правила логики .

В 1936 году Алонзо Черч и Алан Тьюринг опубликовали независимые статьи , показывающие , что общее решение проблемы Entscheidungs те, которые выражаются в лямбда-исчислении ). Это предположение теперь известно как тезис Черча-Тьюринга .

История проблемы

Истоки проблемы Entscheidungsproblem восходят к Готфриду Лейбницу , который в семнадцатом веке, после создания успешной механической вычислительной машины , мечтал построить машину, которая могла бы манипулировать символами, чтобы определять истинностные значения математических утверждений. Он понял, что первым шагом должен быть чистый формальный язык , и большая часть его последующей работы была направлена ​​​​на эту цель. В 1928 году Давид Гильберт и Вильгельм Акерман поставили вопрос в форме, изложенной выше.

В продолжение своей «программы» Гильберт поставил на международной конференции в 1928 году три вопроса, третий из которых стал известен как «проблема Гильберта Entscheidungs ». В 1929 году Мозес Шенфинкель опубликовал статью об особых случаях проблемы принятия решений, подготовленную Полем Бернейсом .

Еще в 1930 году Гильберт считал, что неразрешимой проблемы не существует.

Отрицательный ответ

Прежде чем можно было ответить на этот вопрос, необходимо было формально определить понятие «алгоритм». Это было сделано Алонсо Черчем в 1935 году с концепцией «эффективной вычислимости», основанной на его λ-исчислении , и Аланом Тьюрингом в следующем году с его концепцией машин Тьюринга . Тьюринг сразу понял, что это эквивалентные модели вычислений .

Отрицательный ответ на проблему Entscheidungsproblem был затем дан Алонзо Черчем в 1935–36 годах ( теорема Черча ) и независимо вскоре после этого Аланом Тьюрингом в 1936 году ( доказательство Тьюринга ). Черч доказал, что не существует вычислимой функции , которая бы решала для двух заданных выражений λ-исчисления, эквивалентны они или нет. Он во многом полагался на более ранние работы Стивена Клини . Тьюринг свел вопрос о существовании «алгоритма» или «общего метода», способного решить проблему Entscheidungs , к вопросу о существовании «общего метода», который решает, остановится или нет какая-либо данная машина Тьюринга (проблема остановки ). Если под «алгоритмом» понимать метод, который можно представить в виде машины Тьюринга, и при отрицательном (в общем) ответе на последний вопрос, то вопрос о существовании алгоритма для задачи Entscheidungs ​​также должен быть отрицательным ( в общий). В своей статье 1936 года Тьюринг говорит: «Соответствуя каждой вычислительной машине «оно», мы конструируем формулу «Un(it)» и показываем, что, если существует общий метод определения того, доказуемо ли «Un(it)», тогда существует общий метод определения того, печатает ли он когда-либо 0".

На работу Черча и Тьюринга сильно повлияла более ранняя работа Курта Геделя над его теоремой о неполноте , особенно методом присвоения чисел ( нумерация Геделя ) логическим формулам с целью свести логику к арифметике.

Проблема Entscheidungsproblem связана с десятой проблемой Гильберта , которая требует алгоритма , позволяющего определить, имеют ли диофантовые уравнения решение. Отсутствие такого алгоритма, установленного работой Юрия Матиясевича , Джулии Робинсон , Мартина Дэвиса и Хилари Патнэм с последней частью доказательства в 1970 году, также подразумевает отрицательный ответ на Entscheidungsproblem .

Некоторые теории первого порядка алгоритмически разрешимы; примеры этого включают арифметику Пресбургера , реальные закрытые поля и системы статических типов многих языков программирования . Однако общая теория натуральных чисел первого порядка , выраженная в аксиомах Пеано , не может быть решена с помощью алгоритма.

Практические процедуры принятия решений

Наличие практических процедур принятия решений для классов логических формул представляет значительный интерес для проверки программ и схем. Чисто логические формулы обычно решаются с использованием методов решения SAT, основанных на алгоритме DPLL . Конъюнктивные формулы для линейной вещественной или рациональной арифметики могут быть решены с использованием симплексного алгоритма , формулы в линейной целочисленной арифметике ( арифметика Пресбургера ) могут быть решены с использованием алгоритма Купера или Омега-теста Уильяма Пью . Формулы с отрицаниями, конъюнктами и дизъюнкциями сочетают в себе трудности проверки выполнимости с трудностью решения конъюнкций; в настоящее время они обычно решаются с использованием методов SMT-решения , которые сочетают в себе решение SAT с процедурами принятия решений для соединений и методов распространения. Действительная полиномиальная арифметика, также известная как теория действительных замкнутых полей , разрешима; это теорема Тарского-Зейденберга , которая была реализована в компьютерах с помощью цилиндрического алгебраического разложения .

Вау!! 😲 Ты еще не читал? Это зря!

• Теорема Геделя о неполноте

Исследование, описанное в статье про проблема разрешения , подчеркивает ее значимость в современном мире. Надеюсь, что теперь ты понял что такое проблема разрешения , entscheidungsproblem и для чего все это нужно, а если не понял, или есть замечания, то не стесняйся, пиши или спрашивай в комментариях, с удовольствием отвечу. Для того чтобы глубже понять настоятельно рекомендую изучить всю информацию из категории Языки и методы программирования. Теория трансляции