Математическая логика и теория алгоритмов

Теорема 3.6 (полнота метода резолюций). Множество S дизъюнктов невыполнимо тогда и только тогда, когда существует вы­ вод пустого дизъюнкта • из б" (имеется в виду, что выводом является применение метода резолюций). Существует много различных подходов к построению вывода с помощью метода резолюций. Рассмотрим некоторые из них: метод насыщения уровня, стратегию вычеркивания, лок-резолюцию и один метод для дизъюнктов специального вида. Коль с головой ты в воду погрузился, Не все ли равно, какая глубина? Дикаики § 4. Метод насыщения уровня Ранее был введен метод резолюций и приведена теорема, утверждающая полноту метода резолюций. Пусть имеем множество дизъюнктов S={Dj,Db.'',Dii}. Процедура получения бинарных резольвент неоднозначна, ибо можно сравнивать Dj и 1>2, затем Di и Вз или как-то иначе, Рассмотрим метод насыщения уровня. Он состоит в вычислении всех резольвент всех пар дизъюнктов из S, добавлении этих резольвент к множеству S, вычислении всех следующих резольвент и повторении этого процесса до тех пор, пока не найдется пустой дизъюнкт •, либо будет установлено, что пустой дизъюнкт получить нельзя. Это значит, мы порождаем где 5''=)$',а5"={резольвенты1)уИDj,- Dje{ 5''и5''и...и5""'), n=l,2,... Чтобы запрограммировать этот метод на ЭВМ, можно сперва записать дизъюнкты 5''uiS'u...UiS"'', затем вычислять резольвенты, сравнивая последовательно каждый дизъюнкт D^eOS°u5'^u...u5"'^) с каждым дизъюнктом который расположен после Dj. Когда резольвента вычислена, она присоединяется к концу списка, порож­ денному к этому времени. Перейдем к реализации этого процесса для случая, когда PvQ, 1 PvQ, Pv l Q, 1Pv l Q). 94