Алгоритмическая разрешимость


Алгоритмическая разрешимость

В математической логике и теории алгоритмов под разрешимостью подразумевают свойство формальной теории обладать алгоритмом, определяющим по данной формуле, выводима она из множества аксиом данной теории или нет. Теория называется разрешимой, если такой алгоритм существует, и неразрешимой, в противном случае. Вопрос о выводимости в формальной теории является частным, но вместе с тем, важнейшим случаем более общей проблемы разрешимости.

Содержание

История вопроса и предпосылки

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

Большой прогресс в формализации этих понятий был достигнут в начале XX века Гильбертом и его школой. Тогда, сначала, сформировались понятия исчисления и формального вывода, а затем Гильбертом же, в его знаменитой программе обоснования математики была поставлена амбициозная цель формализации всей математики. Это предусматривало, в том числе, возможность автоматической проверки любой математической формулы на предмет истинности. Отталкиваясь от работ Гильберта Гёдель впервые описал класс так называемых рекурсивных функций, с помощью которой доказал свои знаменитые теоремы о неполноте. Впоследствии был введён ряд других формализмов, таких как машина Тьюринга, λ-исчисление, оказавшихся эквивалентными рекурсивным функциям. В настоящее время, каждый из них считается формальным эквивалентом интуитивного понятия вычислимой функции. Эта эквивалентность постулируется тезисом Чёрча.

Когда понятия исчисления и алгоритма были уточнены, последовал ряд результатов о неразрешимости различных теорий. Одним из первых таких результатов была теорема, доказанная Новиковым, о неразрешимости проблемы слов в группах. Разрешимые же теории были известны задолго до этого.

Интуитивно понятно, что чем сложнее и выразительнее теория, тем больше шансов, что она окажется неразрешимой. Поэтому, грубо говоря, «неразрешимая теория» — синоним к «сложная теория».

Общие сведения

Формальное исчисление в общем случае должно определять язык, правила построения термов и формул, аксиомы и правила вывода. Таким образом, для каждой теоремы T, всегда можно построить цепочку A1, A2, … , An=T, где каждая формула Ai либо является аксиомой, либо выводима из предыдущих формул, по одному из правил вывода. Разрешимость означает, что существует алгоритм, который для каждого правильно построенного предложения T, за конечное время выдаёт однозначный ответ: да, данное предложение выводимо в рамках исчисления или нет — оно не выводимо.

Очевидно, что противоречивая теория разрешима, так как любая формула будет выводимой. С другой стороны, если исчисление не обладает рекурсивно перечислимым множеством аксиом, как например, логика второго порядка, оно, очевидно, не может быть разрешимым.

Примеры разрешимых теорий

DLO-теория днища,про которую знает только Стукачев Алексей Ильич

Примеры неразрешимых теорий

Полуразрешимость и автоматическое доказательство

Разрешимость — очень сильное свойство, и большинство полезных и используемых на практике теорий им не обладают. В связи с этим было введено более слабое понятие полуразрешимости. Полуразрешимость означает наличие алгоритма, который за конечное время всегда подтвердит, что предложение истинно, если это действительно так, но если нет — может работать бесконечно.

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

Большое практическое значение имеют эффективные полуразрешающие процедуры для логики первого порядка, так как они позволяют (полу)автоматически доказывать формализованные утверждения очень широкого класса. Прорывом в этой области было открытие Робинсоном в 1965 году метода резолюций. Другим важнейшим полуразрешающим алгоритмом на сегодняшний день является табло-метод.

Связь разрешимости и полноты

В математической логике, традиционно используется два понятия полноты: собственно полнота и полнота, относительно некоторого класса интерпретаций (или структур). В первом случае, теория полна, если любое предложение в ней является либо истинным, либо ложным. Во втором — если любое предложение, истинное при всех интерпретациях из данного класса выводимо. Например, натуральная арифметика неполна, согласно теоремам Гёделя о неполноте, но она полна относительно своей стандартной интерпретации — это следует из теоремы Гёделя о полноте.

Оба понятия тесно связаны с разрешимостью. Например, если множество аксиом полной теории первого порядка рекурсивно перечислимо, то она разрешима. Это следует из известной теоремы Поста, утверждающей, что если множество и его дополнение оба рекурсивно перечислимы, то они также рекурсивны. Интуитивно, аргумент, показывающий истинность приведённого утверждения следующий: если теория полна, и множество её аксиом рекурсивно перечислимо, то существуют полуразрешающие процедуры, для проверки истинности любого утверждения, равно как и его отрицания. Если запустить обе эти процедуры параллельно, то учитывая полноту теории, одна из них должна когда-нибудь остановиться и выдать позитивный ответ.

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

См. также

Литература

  • Мальцев А. И., Алгоритмы и рекурсивные функции, Наука, 1986.
  • Ackermann W., Solvable Cases of the Decision Problem, North-Holland Publishing, Amsterdam, 1954.
  • John Alan Robinson, Andrei Voronkov (Eds.): Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press 2001, ISBN 0-444-50813-9, ISBN 0-262-18223-8

Wikimedia Foundation. 2010.

Смотреть что такое "Алгоритмическая разрешимость" в других словарях:

  • АЛГОРИТМИЧЕСКАЯ ПРОБЛЕМА — проблема, в к рой требуется найти единый метод ( алгоритм).для решения бесконечной серии однотипных единичных задач. Такие проблемы иногда наз. также массовыми проблемами. А. п. возникали и решались в различных областях математики на протяжении… …   Математическая энциклопедия

  • АЛГОРИТМИЧЕСКАЯ СВОДИМОСТЬ — одно из основных понятий алгоритмов теории и ее приложений Возникло в связи с тем, что неразрешимость (и разрешимость) многих алгоритмических проблем устанавливается большей частью не непосредственно, а путем сведения к исследуемой проблеме такой …   Математическая энциклопедия

  • Алгоритмически неразрешимая задача — В теории вычислимости алгоритмически неразрешимой задачей называется задача, имеющая ответ да или нет для каждого объекта из некоторого множества входных данных, для которой (принципиально) не существует алгоритма, который бы, получив любой… …   Википедия

  • Разрешение — Разрешение: Разрешение сделать что то  антоним к слову «запрет». Позволение сделать что то запрашиваемое, в том числе документ, это подтверждающий; Разрешение на работу; Разрешение на временное проживание; Разрешение на поселение; Разрешение …   Википедия

  • Клеточный автомат — дискретная модель, изучаемая в математике, теории вычислимости, физике, теоретической биологии и микромеханике. Включает регулярную решётку ячеек, каждая из которых может находиться в одном из конечного множества состояний, таких как 1 и 0.… …   Википедия

  • Открытые математические проблемы — Открытые (нерешённые) математические проблемы  проблемы, которые рассматривались математиками, но до сих пор не решены. Часто имеют форму гипотез, которые предположительно верны, но нуждаются в доказательстве. В научном мире популярна… …   Википедия

  • Клеточные автоматы — Клеточный автомат (КА)  набор клеток, образующих некоторую периодическую решетку с заданными правилами перехода, определяющими состояние клетки в следующий момент времени через состояние клеток, находящимися от нее на расстоянии не больше… …   Википедия

  • Робинсон, Джон Алан — Джон Алан Робинсон John Alan Robinson …   Википедия

  • Проблема разрешимости — Проблема разрешимости  вопрос, сформулированный в рамках какой либо формальной системы, требующий ответа «да» или «нет», возможно, зависящего от значений некоторых входных параметров. Например, проблема «дано два числа x и y, делится ли x на …   Википедия

  • Алгоритм Тарского — Алгоритм Тарского  универсальный алгоритм, позволяющий установить истинность или ложность любой замкнутой арифметической формулы первого порядка с переменными для вещественных чисел. Алгоритм Тарского позволяет проверить истинность или… …   Википедия