11.Проблема разрешимости

Пусть дана произвольная формула A(X1,…,Хn). Можно ли как-то проверить, что она является общезначимой? Если существует такой способ (алгоритм), позволяющий в конечное число шагов убедиться в этом, то говорят, что проблема проверки общезначимости формул алгебры высказываний разрешима.

Теорема 1.3. Проблема разрешимости в алгебре высказываний имеет положительное решение.

Доказательство. Рассматривая набор переменных (X1,…,Хn) на множестве { _|_, Т}, имеем 2 в степени n возможных комбинаций. Для каждой комбинации легко вычислить истинностное значение формулы А. Это можно сделать, написав программу для компьютера. Найдя все значения формулы, мы узнаем всегда ли она истинна. Если «да», то формула А общезначима.

Теорема 1.3 доказана.

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