Табличный способ решения проблемы разрешимости.

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

Например, проблема «дано два числа x и y, делится ли x на у?» является проблемой разрешимости. Ответ может быть дан либо «да» либо «нет» и зависит от значений xи y. Метод решения проблемы разрешимости, представленный в форме алгоритма, называется разрешающей процедурой для этой проблемы. Так, разрешающая процедура для проблемы разрешимости «дано два числа x и y, делится ли нацело x на у?» должна определять совокупность действий, которые следует предпринять для проверки делимости нацело x на у для данных x и y. Один из таких алгоритмов деление столбиком изучается в начальной школе. Остаток равный нулю означает ответ «да», иначе «нет». Проблема разрешимости, для которой существует разрешающая процедура, называется разрешимой.

Исследования в области теории рекурсии часто сфокусированы на проблемах разрешимости, поскольку к ним без потери общности сводятся многие задачи.

разрешения проблема (разрешимости проблема) - проблема

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

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

Невозможность найти для теории общий разрешающий метод не исключает поиска процедуры разрешения для отдельных классов ее

утверждений.

СОКРАЩЕННЫЙ СПОСОБ РЕШЕНИЯ ПРОБЛЕМЫ РАЗРЕШИМОСТИ.

Все формулы алгебры логики делятся на три класса:

1)тождественно истинные,

2)тождественно ложные

3)выполнимые.

Формулу А называют тождественно истинной, если она при всех значениях входящих в неё переменных высказываний принимает значение 1(истина). Формулу А называют тождественно ложной, если она при всех значениях входящих в неё переменных принимает значение 0(ложь).Формулу A называют выполнимой, если она принимает значение 1(истина), хотя бы на одном наборе входящих в нее переменных и не является тождественно истинной.

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

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

Однако практическое использование таблицы истинности для формулы при больших n затруднительно.

Существует другой способ, позволяющий, не используя таблицы истинности, определить, к какому классу относится формулаА. Этот способ основан на приведении формулы к нормальной форме (КНФ или ДНФ) и использовании алгоритма, который позволяет определить, является ли данная формула тождественно истинной или не является. Одновременно с этим решается вопрос о том, будет ли формула А выполнимой.

ОСНОВНЫЕ ЛОГИЧЕСКИЕ ВЫВОДЫ.

Правило вывода – это предписание, или разрешение позволяющее из суждения 1-ой логической структуры, как посылок, вывести суждения некоторой логической структуры, как заключения.

Особенности правил заключения в том, что признаки истинности заключения производятся на основе не содержания, а их структуры. Правила вывода записываются в виде схемы, которая состоит из 2-ух частей (сверху и снизу), разделённых вертикальной линией. Над чертой в столбец записываются логические схемы посылок, под чертой логические схемы заключения.

Все правила выводов логики высказываний делятся на 2-е группы:

Основные и Производные.

• Основные – это простые и очевидные правила, не нуждающееся в доказательстве. Основные делятся на прямые и косвенные.

• Прямые – это такие правила, которые указывают на непосредственно выводимость одних суждений из других.

• Косвенные – лишь дают возможность умозаключить о правомерности вывода одних суждений из других.

• Производные - сокращённый процесс вывода, выводятся из основных.

ВЫВОД ЛОГИЧЕСКИЙ – рассуждение, в котором осуществляется переход по правилам от высказывания или системы высказываний к высказыванию или системе высказываний. К логическому выводу обычно предъявляются (совместно или по отдельности) следующие требования: 1) правила перехода должны воспроизводить отношение следования логического (ту или иную его разновидность); 2) переходы в логическом выводе должны осуществляться на основе учета только синтаксических характеристик высказываний или систем высказываний.

В современной логике понятие логического вывода определяется для формальных систем, в которых высказывания представлены формулами. Обычно выделяют три основных типа формальных систем: аксиоматические исчисления, исчисления натурального вывода, исчисления секвенций. Стандартное определение логического вывода (из множества формул Г) для аксиоматического исчисления S таково: логический вывод в S из множества формул Г есть такая последовательность Α1... Аn формул языка исчисления S, что для каждой Ai (1 ≤i ≤n) выполняется, по крайней мере, одно из следующих трех условий: 1) Ai есть формула из Г; 2) Ai есть аксиома исчисления S; 3) Ai есть формула, получающаяся из предшествующей ей в последовательности А1...Аn формулы или из предшествующих ей в этой последовательности формул по одному из правил вывода исчисления S. Если α есть логический вывод в S из множества формул Г, то формулы из Г называются посылками a, a сам вывод α называется выводом в S из посылок Г; если при этом А есть последняя формула α, то α называется логическим выводом в S формулы А из посылок Г.Запись «Г ⊦sA» означает, что существует логический вывод в S формулы А из посылок Г. Логический вывод в S из пустого множества формул называется доказательством в S. Запись «⊦sA» означает, что существует доказательство в S формулы А. Формула А называется доказуемой в S,если⊦A. В качестве примера рассмотрим аксиоматическое исчисление S1 со стандартным определением вывода, являющееся вариантом классической логики высказываний. Алфавит этого исчисления содержит только пропозициональные переменные р1, р2, ..., рn, ..., логические связки ⊃, ⌉ и круглые скобки.