Связь между общезначимостью и выполнимостью формул логики предикатов.
Теорема 1. Для того, чтобы формула F была общезначимой, необходимо и достаточно, чтобы её отрицание было не выполнимо.
Теорема 2. Для того, чтобы формула F была выполнима, необходимо и достаточно, чтобы формула была не общезначима.
Проблема разрешения для общезначимости и выполнимости формул.
Постановка проблемы и её неразрешимость в общем виде: в алгебре высказываний было установлено, что существует четкий алгоритм, позволяющий для любой формулы алгебры высказываний ответить на вопрос, будет ли данная формула выполнима, тождественно истинна или тождественно ложна. Для этого нужно составить ТИ (таблица истинности) формулы и посмотреть на распределение нулей и единиц в её последнем столбце. Аналогичная проблема возникает и для формул логики предикатов: существует ли единый алгоритм, позволяющий для любой формулы логики предикатов определить, будет ли она выполнимой или общезначимой? Ответ отрицательный: общего такого алгоритма не существует. Это было доказано в 1936 г. Американским ученым А. Черчем.
Для некоторых частных видов формул данная проблема допускает решение.
Решение проблемы для формул на конечных множествах.
Пусть формула логики предикатов рассматривается на конечном множестве. Вместо её предикатных переменных подставляем конкретные предикаты, определенные на этом конечном множестве. Т.к. операции квантификации сводятся к конъюнкции и к дизъюнкции
,
то задача о выполнимости и общезначимости формулы логики предикатов на конечном множестве сводится к задаче о выполнимости или общезначимости некоторой формулы алгебры высказываний. А эта задача разрешима.
Продемонстрируем идею действия этого алгоритма на конкретном примере. Рассмотрим формулу логики предикатов
и выясним, будет ли она выполнима или общезначима на двухэлементном множестве .
Do'stlaringiz bilan baham: |
