Алгоритмы распознавания общезначимости формул логики высказываний

В случае логики высказываний проверка общезначимости формулы, имеющей п переменных, может быть осуществлена путем перебора всех 2^П возможных наборов логических констант, сопоставляемых этим переменным при различных интерпретациях, и установлении того, что все значения формулы на этих наборах равны И. Таким образом здесь имеется не только алгоритм перечисления всех общезначимых формул, но и алгоритм проверки общезначимости. Однако даже для такого простейшего случая остается проблема уменьшения трудоемкости распознавания общезначимости по сравнению с практически малоприемлимым для сколь-нибудь значительных п перебором всех 2^П наборов значений переменных. К проблеме распознавания общезначимости формул логики высказываний тесно примыкает проблема решения систем логических уравнений сводящаяся к нахождению всех наборов значений переменных при которых заданная формула алгебры логики принимает значение И. Последняя проблема часто встречается в различных прикладных задачах дискретной оптимизации и диагностики, и поиску эффективных процедур решения ее, учитывающих в своих эвристических решающих правилах статистические особенности рассматриваемого класса задач, посвящено большое количество исследований. Мы ограничимся здесь лишь несколькими простейшими процедурами подобного рода (применительно к задаче распознавания общезначимости), поскольку они позволят нам развить технику доказательства теорем в логике высказываний, представляющую собой упрощенный аналог техники, развиваемой далее для автоматического доказательства теорем в логике предикатов.

Прежде всего, опишем алгоритм Квайна, осуществляющий проверку общезначимости формулы / логики высказываний при помощи построения так называемого семантического дерева. Корню этого дерева — исходной вершине — приписывается формула /. Пусть уже построено некоторое подмножество вершин семантического дерева, каждой из которых сопоставлена некоторая формула. Если каждой концевой вершине данного дерева оказалась сопоставлена константа И, то процесс завершается, и формула / является общезначимой. Если некоторой концевой вершине дерева сопоставлена константа Л, то формула / не общезначима, и процесс также завершается. В противном случае найдется концевая вершина г>, которой сопоставлена формула отличная от констант И, Л. Если эта формула д не содержит переменных, то ее можно преобразовать в логическую константу, используя тождества:

Если же она содержит хотя бы одну переменную х, и выполняются следующие действия:

• а) Находятся результаты д и д^ подстановки в формулу д вместо переменной х, соответственно констант И и Л.
• б) Находятся результаты д и д'₂ упрощения формул д и <72 при помощи перечисленных выше тождеств, применяемых до тех пор пока это возможно.
• в) вводятся две новые вершины Vi и v₂ семантического дерева, которым приписываются, соответственно, формулы д и д₂. К этим вершинам от вершины v проводятся ребра, отмеченные соответственно выражениями х = И и х = Л.

Далее повторяется описанный выше процесс рассмотрения концевых вершин семантического дерева.

В данной процедуре остался недоопределенным выбор конкретной переменной х формулы д, по которой проводится «разбор случаев». Этот выбор в прикладных программах, решающих системы логических уравнений путем построения семантических деревьев, осуществляется на основании различных эвристических решающих правил. Простейшим таким правилом является выбор переменной, имеющей наибольшее число вхождений в <7, для получения наиболее сильного упрощения при переходе к д[ и д₂, другим полезным соображением является такой выбор переменных х, при котором сопоставленные концевым вершинам семантического дерева формулы д оказывались бы представимы, например, как hi&ch₂ либо hi V /12, где формулы h и h₂ не имеют общих переменных. В этом случае вместо.

Рис. 3.1: Алгоритм Квайна.

построения ветви дерева для Л1&Л2 (Л1 V Л2, h —> /12 и т. п.) можно было бы рассмотреть независимо формируемые деревья для Ль Л₂ и из анализа их концевых вершин сделать вывод относительно общезначимости д.

Пример. В качестве примера применения алгоритма Квайна убедимся в общезначимости формулы, полученной из схемы аксиом А2:

Дерево разбора случаев для этой формулы приведено на рисун;

ке 3.1.

В прикладных ситуациях логические языки редко используются во всем многообразии своих синтаксических возможностей. Обычно их формулы приводятся эквивалентными преобразованиями к тому или иному «стандартному виду», который и сохраняется в процессе обработки информации. С точки зрения логики высказываний, наиболее типичной логической стандартной формой, отражающей тенденцию к описанию ситуаций в виде конъюнкции условий, является конъюнктивная нормальная форма. Формула, представленная, в этой форме, имеет вид Ai&…&A_n, n > 1, где каждое (г = — формула вида (В_а V • • • V где mi > 1, причем (Вц,…, B_imj —.

переменные или отрицания переменных.

Более точно, для определения конъюнктивной нормальной формы введем сначала понятие дизъюнкта. Если Хь…, x_m — различные переменные, т > 1, то формулу вида (x°^l V • • • VxJ?") назовем дизъюнктом. Логическую константу Л по определению так же считаем дизъюнктом.

Если Ль…, А_п — различные дизъюнкты (n > 1), то формула (Л1&. .&Л_П) называется конъюнктивной нормальной формой.

Произвольную формулу логики высказываний можно преобразовать к виду конъюнктивной нормальной формы, используя следующие эквивалентные преобразования:

а) логические связки —?, «-> устраняются при помощи тождеств.

б) отрицания в формуле ''опускаются до переменных" при помощи тождеств.

в) применяются преобразования дистрибутивности:

г) устраняются повторные вхождения переменных в дизъюнктивных подформулах, а также константы И, Л (если сама формула не есть И или Л):

д) устраняются одинаковые дизъюнкты: а&а = а.

В процедурах автоматического доказательства теорем часто применяется метод доказательства «от противного». В этом случае для доказательства общезначимости формулы / переходят к рассмотрению формулы -*/ и пытаются доказать ее невыполнимость.

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

Первоначально вводим корень семантического дерева и сопоставляем ему множество дизъюнктов формулы д.

Пусть уже построена часть семантического дерева.

Если концевой вершине дерева сопоставлено пустое множество дизъюнктов (пустое множество соответствует логической константе И), то формула д — выполнима, и алгоритм прекращает работу.

Если каждой концевой вершине семантического дерева соответствует множество дизъюнктов, содержащее дизъюнкт Л, то формула д — невыполнима, и алгоритм прекращает работу.

Если некоторой концевой вершине v сопоставлено непустое множество дизъюнктов S, не содержащее дизъюнкта Л, то в S входят дизъюнкты с переменными. Выбираем одну из таких переменных х и разбиваем S на три подкласса: S — все дизъюнкты, в которые х входит без внешнего отрицания, 5 г — все дизъюнкты, в которые х входит с отрицанием, S3 — все дизъюнкты в которых х не встречается. Далее рассматриваем множество дизъюнктов S_x = {dd V -«х € S2} (если ->х € S2, то здесь берется d = Л) и множество дизъюнктов и множество дизъюнктов S-,_z = {dd V х G Si} (если х? Si, то здесь берется d = Л). Нетрудно видеть, что невыполнимость конъюнкции дизъюнктов списка S эквивалента одновременной невыполнимости конъюнкций дизъюнктов списков S_x U S3 и S-,_x U S3. Поэтому для продолжения построения семантического дерева вводим две новых вершины v и V2, которым сопоставляем, соответственно, множества дизъюнктов S_zuS3 и 5-,_zUS3, причем проводим к Vi и г>2 ребра от v, отмеченные соответственно выражениями х = И и х = Л.

Далее повторяется описанный выше процесс рассмотрения концевых вершин семантического дерева.

Пример. В качестве примера применения модифицированного алгоритма Квайна обратимся опять к формуле /, заданной выражением (3.1). После устранения логических связок —" мы получим формулу.

Далее переходим к рассмотрению формулы которая имеет вид:

Рис. 3.2: Модифицированный алгоритм Квайна. Семантическое дерево для формулы ->д приведено на рисун;

ке 3.2.

Другой алгоритм распознавания невыполнимости конъюнктивной нормальной формы связан с рассмотрением специальной дедуктивной системы, использующей в качестве правила вывода так называемое правило резолюции. В этом случае конъюнктивная нормальная форма снова представляется как множество своих дизъюнктов, эти дизъюнкты и образуют перечень аксиом данной дедуктивной системы. Правило резолюции будучи применено к двум дизъюнктам АУ В и ->А У С создает в качестве следствия новый дизъюнкт В У С (здесь возможны вырожденные случаи отсутствия В либо С, если они оба отсутствуют, то результатом служит дизъюнкт Л). Достаточность применения данного правила вывода для распознавания невыполнимости гарантируется следующим утверждением. Теорема 20. Конъюнкция конечного семейства дизъюнктов S невыполнима тогда и только тогда, когда за конечное применений правила резолюции из S выводится дизъюнкт Л.

Доказательство. Доказывать будем индукцией по числу п переменных, встречающихся в дизъюнктах из 5.

Базис индукции. Если п = 0, то утверждение очевидно, так как в этом случае непустое семейство дизъюнктов может содержать только логическую константу Л.

Индуктивный переход. Пусть утверждение уже доказано для некоторого п.

Рассмотрим семейство S с n+1 переменной: х, Х2,…, x_n+i • Разобьем S на три подкласса: Si — все дизъюнкты представимые в виде x_n+i V а, — все дизъюнкты представимые в видечх_п+1 V 6, S3 — дизъюнкты не содержащие x_n+i*.

Дизъюнкты множества.

получены из дизъюнктов семейства S применением правила резолюции (здесь допускаются вырожденные случаи, когда а либо b отсутствует, причем при одновременном отсутствии а и Ь в Я включается константа Л).

Рассмотрим семейство дизъюнктов Я U S3 и покажем, что его невыполнимость эквивалентна невыполнимости S. Если S выполнимо, то интерпретация, обращающая в И дизъюнкты из S дает значения И и для всех дизъюнктов из R U S3, т. е. R U S₃ выполнимо. Пусть S невыполнимо, рассмотрим набор истинностных значений оч,…, а_п переменных xi_f.,~, z_n и покажем, что на этом наборе хотя бы один из дизъюнктов семейства R U 5з имеет значение Л. Так как S невыполнимо, то на наборе а_ь…, а_п, И значений переменных Xi,…, x_n, x_n+1 некоторый дизъюнкт d из S имеет значение Л. Если d € S3, то он и является искомым дизъюнктом в Я U S3. Так как x_n+i имеет значение И, то при d ? S3 остается единственная возможность d € S2, т. е. d = «^,x_n+i V 6. Аналогично на наборе оч,…, а», Л значений переменных х_%…, x_n, x"+i некоторый дизъюнкт в! из S имеет значение Л. Снова, если d' 6 S3, то он и есть искомый, а в противном случае (так как x_n+i имеет значение Л) необходимо d' ^ Siy то есть d' = x_n+i Va. Дизъюнкты, а и 6 не содержат переменной x_n+i, и поэтому оба принимают значение Л, если переменные xi,…, х_п имеют значения ац,…, a_n. Следовательно и дизъюнкт d" = aV&, принадлежащий Я, будет иметь на наборе оч,…, а" значений переменных xi,…, х_п значение Л. Это и означает доказательство эквивалентности невыполнимости S и Я U S3.

Но число переменных в RL)S$ не более п, т. е. для него имеет место эквивалентность невыполнимости и существования вывода константы Л.

Если константа Л выводима из S, то либо дизъюнкт Л принадлежит S, и тогда S — невыполнимо, либо константа Л выводима из Я U S3, тогда Л U S3 — невыполнимо и, следовательно, S — невыполнимо.

Если S невыполнимо, то невыполнимо Ли S3 и из Ли S3, а, значит, и из S выводима константа Л.

Тем самым теорема доказана. ?

Пример. В качестве примера применения правила резолюции обратимся опять к формуле ->д_} заданной выражением (3.2). Исходное множество дизъюнктов имеет вид.

Из (->xi V Х2) и х по правилу резолюции выводится х2. Из (-ЧГ1 VЧГ2 V Хз) и Х ВЫВОДИМ -1X2 V Х3. Из (««Х2 V Х3) И Хг выводим Х3. И наконец, из хз и -«хз получаем Л. Следовательно, формула -уд невыполнима.

Упражнения.

3.1. Какие из следующих выражений являются правильными выражениями (формулами) логики высказываний:

• 3.2. Расставьте скобки в следующих выражениях (с учетом приоритета операций &, V, —?,"-+ и левой ассоциативности всех двухместных операций), так чтобы получились правильные выражения логики высказываний:
• 3.3. Какие из следующих формул логики высказываний общезначимы, а какие — выполнимы:

3.4. Построить таблицу истинности для следующих формул логики высказываний:

• 3.5. Для каждой выполнимой формулы из упражнений 3.3 и 3.4 найти хотя бы одну ее модель.
• 3.6. Для каждой формулы из упражнений 3.3 и 3.4 проверить является ли она выполнимой, невыполнимой, общезначимой с помощью метода Квайна, модифицированного метода Квайна и метода резолюции.
• 3.7. Докажите эквивалентность следующих формул логики высказываний:

3.8. Докажите леммы 11, 12 и 13.

3.9. Пусть f, g_th — формулы логики высказываний. Докажите справедливость следующих утверждений: