Материал: Алгебра_кортежей

4) каждому m-местному предикату соответствует некоторое отношение на

Am.

Am – m-кратное декартово произведение множества A.

Каждой формуле исчисления предикатов равносильно некоторое (возможно, пустое) многоместное отношение, задающее ее область истинности. Состав атрибутов этого отношения соответствует составу свободных переменных в исходной формуле [Мендельсон, 1984].

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

Разумно предположить, что выполнимость формул, у которых предикаты соединены логическими связками, например, P(x, z) Q(y, z), можно вычислить алгебраически как результат операций над соответствующими многоместными отношениями. В частности, для данного примера интерпретацией исходной формулы целесообразно считать отношение, вычисляемое как P[XZ] Q[YZ], где P[XZ] – отношение, соответствующее области истинности предиката P(x, z), а Q[YZ] – отношение, соответствующее области истинности предиката Q(y, z). Тогда, если выражение P[XZ] Q[YZ] = , то формула P(x, z) Q(y, z) невыполнима. Однако, запись P[XZ] Q[YZ] в общем случае некорректна, поскольку отношения P и Q заданы в различных схемах, а операции алгебры множеств над такими отношениями не определены.

Прежде чем приступить к изложению принципа резолюции, введем несколько определений.

В исчислении высказываний можно выделить классы формул, обладающих полезными свойствами [Яблонский, 1966]. Среди них наибольший интерес представляют два универсальных класса – дизъюнктивная нормальная форма

50

(ДНФ) и конъюнктивная нормальная форма (КНФ). Кроме ДНФ и КНФ,

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

Литералом называется формула, которая состоит либо из одного атома, либо из отрицания атома.

Конъюнкт – это формула, состоящая из одного литерала или конъюнкции произвольного числа литералов.

Дизъюнкт есть формула, состоящая из одного литерала или дизъюнкции произвольного числа литералов.

Например, формула B C D – конъюнкт, а A B D – дизъюнкт. В то же время формулу D можно интерпретировать как конъюнкт или как дизъюнкт. Теперь можно перейти к определениям универсальных классов.

Дизъюнктивная нормальная форма – это дизъюнкция произвольного числа конъюнктов.

Конъюнктивная нормальная форма есть конъюнкция произвольного числа дизъюнктов.

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

1)заменить все литералы в исходной формуле на противоположные (т.е. литерал X преобразуется в литерал X, а литерал Y – в литерал Y);

2)заменить все присутствующие в исходной формуле логические связки " " на связки " ", а все связки " " – на связки " ".

Например, если исходная формула есть ДНФ

( B) (A B C) ( A C),

то после приведенных выше преобразований получим формулу

(B) ( A B C) (A C),

представляющая отрицание предыдущей формулы в виде КНФ.

Изложенное справедливо и для отрицания формулы, выраженной в виде КНФ. Те же преобразования позволяют получить ее отрицание в виде ДНФ. Данное соотношение основано на многократном применении законов де

51

Моргана.

В исчислении высказываний и предикатов имеется своеобразный "полиморфизм", когда эквивалентные формулы выражаются по-разному (например, A C = A C). Подобный "полиморфизм", хотя и в меньшей степени, может существовать и в пределах одного класса формул, в частности, для формул классов КНФ и ДНФ. Например, с помощью табличного метода можно убедиться, что две ДНФ (A B C) ( A C) и ( A B C) ( B C) эквивалентны.

Теперь рассмотрим принцип резолюции, который применяется для автоматического доказательства теорем и сводится к определению выполнимости или невыполнимости КНФ.

Принцип резолюции имеет определенные преимущества по сравнению с другими методами логического вывода и широко применяется в машинных реализациях систем искусственного интеллекта. Он опирается на теорему 1.6. Для формул исчисления высказываний суть этого принципа состоит в следующем. Последовательность формул F1, ..., Fn, G (см. теорему 1.6) путем применения тождеств алгебры логики преобразуется в некоторое множество непустых дизъюнктов (предполагается, что эти дизъюнкты соединены друг с другом связкой " ", то есть представляют собой КНФ). Затем выбираются пары дизъюнктов, в одном из которых содержится некоторый литерал, а в другом – его отрицание. Доказано, что следствие этой пары дизъюнктов есть дизъюнкт, содержащий все ее литералы, кроме контрарных. Например, если использовать принцип резолюции к паре дизъюнктов A B C и B C , то, удаляя из них контрарные литералы C и C и объединяя оставшиеся, получим в качестве следствия дизъюнкт A B .

Далее новый дизъюнкт приписывается к исходному множеству дизъюнктов, и вывод продолжается до тех пор, пока не будет получен пустой дизъюнкт (в этом случае вывод был корректным), либо окажется, что пустой дизъюнкт получить невозможно (тогда вывод не подтверждается).

Рассмотрим пример. Пусть требуется методом резолюций доказать или опровергнуть корректность вывода

A, B C, A B C ├ A B .

Применив теорему 1.6 и закон де Моргана к отрицанию формулы A B ,

52

получим КНФ, которую можно представить как множество дизъюнктов:

1)A;

2)B C;

3)A B C ;

4)A B.

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

5)B C (по принципу резолюции из 1 и 3);

6)B (по принципу резолюции из 2 и 5);

7)B (по принципу резолюции из 1 и 4);

8)пустой дизъюнкт (по принципу резолюции из 6 и 7).

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

необходимо предварительно выполнить ряд преобразований с целью получения бескванторной КНФ. Эти методы подробно описаны в [Чень, 1983] и сопровождаются многочисленными примерами.

Итак, в рамках формального подхода процедура логического вывода часто сводится к задаче анализа выполнимости КНФ, решения которой породили целое направление в математической логике и в Computer science. Речь идет о направлении, которое называется "вычислительная сложность алгоритмов".

1.3.4. Сложность алгоритмов логического вывода (задача "выполнимость КНФ")

Уже на первых этапах разработки программных систем, в частности систем искусственного интеллекта, начали появляться задачи, которые даже при небольшом числе исходных данных были практически нереализуемыми изза громадного объема требуемых вычислительных операций. Возникла проблема классификации задач по степени сложности. Первые результаты в этом направлении были получены Г.С. Цейтиным в конце 50-х годов [Яновская, 1959], но по ряду причин не стали широко известными. Исходным пунктом дальнейших исследований по теории сложности вычислений стали работы М.О. Рабина [Rabin, 1960], Ю. Хартманиса и Р.Е. Стирнза [Hartmanis, 1967], в

53

которых достаточно четко обозначилась постановка проблемы. Интенсивное развитие этой теории началось после опубликования в 1971 и 1972 гг. двух статей С.А. Кука [Cook, 1971] и Р.М. Карпа [Karp, 1972].

Кратко результат работы С.А. Кука заключается в следующем. В основу теории NP-полноты положен класс задач NP (Nondeterministically Polynomial).

Он состоит из задач распознавания, то есть задач, где возможны только два варианта ответа ("да" или "нет"), и содержит не только задачи, решаемые за время, выраженное полиномом фиксированной степени от длины входного предложения, но и задачи, для которых полиномиальный алгоритм решения в общем случае неизвестен. В своей статье С.А. Кук доказал, что любую задачу класса NP можно при использовании рациональной системы кодирования представить в виде некоторой КНФ, при этом преобразование условий любой задачи класса NP в КНФ занимает полиномиальное время. Таким образом, основной NP-полной задачей, стала считаться задача проверки выполнимости заданной КНФ (сокращенно SAT). Суть проблемы, которая носит название выполнимость КНФ, заключается в том, что требуется построить универсальный алгоритм, с помощью которого для любой КНФ можно было бы определить, выполнима данная формула или нет (имеется ли хотя бы один набор значений переменных, при котором формула является истинной).

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

Теперь, чтобы доказать, что некоторая задача T относится к классу NP-полных задач, необходимо: 1) доказать ее принадлежность классу NP; 2) выбрать известную NP-полную задачу и доказать, что эта задача может быть за полиномиальное время преобразована в T. В работе С.А. Кука было также доказано, что к классу NP-полных задач помимо SAT относятся еще две задачи класса NP. Р.М. Карп в своей статье дополнил этот список еще двадцатью широко известными задачами.

Аналогичные результаты независимо и немного позднее были получены в

54