Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

Методом резолюций называется последовательное получение бинарных резольвент из данных дизъюнктов и вновь получаемых дизъюнктов. Пусть, например, даны дизъюнкты di =PVT, d2= —\PVT, d3= —\Т. ИспользуяDj и D2 затем Dj и D3 , получим резольвенты D4=T, DS=P. Затем ш Вз и D4 получим пустой дизъюнкт . Можно доказать следующую теорему. Теорема 3.6 (полнота метода резолюций). Множество S дизъюнктов невыполнимо тогда и только тогда, когда существует вывод пустого дизъюнкта из S (имеется в виду, что выводом является применение метода резолюций). Таким образом, для выяснения будет ли В логическим следствием из нужно построить указанным способом множество дизъюнктов {Di,D2,...,Dk} и применить к нему метод резолюций. Существует много различных подходов к построению вывода с помощью метода резолюций. Рассмотрим некоторые из них: метод насыщения уровня, стратегию вычеркивания, лок-резолюцию и один метод для дизъюнктов специального вида. § 3. Метод насыщения уровня Ранее был введен метод резолюций и приведена теорема, утверждающая полноту метода резолюций. Пусть имеем множество дизъюнктов S={Di,D2,...,Dk}. Процедура получения бинарных резольвент неоднозначна, ибо можно сравнивать Dj и Z)^, затем Djv^Ds или как-то иначе. Рассмотрим метод насыщения уровня. Он состоит в последовательном 0 12 пЗ построении множеств S ,S ,S ,S^,... следующим образом: 1) 2) если построено, то 5"={резольвенты Dj и Dj^: j<k таких, что DjE{ ^uS^u... DkE^-^ }, п=1,2,... Чтобы реализовать этот метод, нужно последовательно выбирать каждый дизъюнкт Z)je(5^ US^ и... uS"'^) и сравнивать с каждым дизъюнктом D^eS^'^, j<k. Когда резольвента вычислена, она присоединяется к концу списка, порожденному к этому времени. Перейдем к реализации этого процесса для случая, когда S={ Р vQ, —Р vQ, Pv^Q,^v^Q}. S": {\)PvQ; i2)^vQ; {3)Pv^Q; 63