12.5. Семантические стратегии

12.5.0. Общие понятия

Если множество предложений выполнимо, то при некотором присваивании значений истинности атомам в все предложения в также выполнимы. Любое конкретное присваивание значений истинности атомам называется моделью. Задача семантических

стратегий состоит в том, чтобы доказать невыполнимость показав, что не существует модели, при которой выполнимо. Можно было бы указать взаимосвязь между исключением моделей и линейными стратегиями, учитывающими ход вывода (Лавленд, 1972), но объяснение было бы слишком техничным. Идею семантического доказательства мы проиллюстрируем эвристическим описанием процедуры доказательства теорем, впервые предложенной Хэйесом и Ковальским (1969). Прежде всего расширим понятие модели.

Пусть — множество элементарных высказываний в и предложений, выводимых из . В общем случае А будет бесконечным счетным множеством. Пусть — множество литералов, выводимых из А, т. е. элементов множества А и их дополнений. Частичной моделью М множества назовем подмножество множества не содержащее одновременно литерала и его дополнения. Потребуем, чтобы в случае, когда модель не содержала ни для какой подстановки Тогда частичная модель будет непротиворечивым присваиванием значений истинности некоторым литералам из Можно считать, что определяет множество моделей элементами которого служат другие модели, включающие в качестве подмножества своих литералов все литералы из или литералы, полученные из них подстановкой. Для иллюстрации предположим, что

Атомы множества А являются подстановочными частными случаями множества Здесь А — бесконечное счетное множество, так как оно состоит из атомов вида Множество состоит из элементов множества А и их дополнений, так что оно тоже бесконечно и счетно. Рассмотрим две неполные модели

Пусть — множество всех полных моделей, включающих как подмножество, а — множество полных моделей, включающих как подмножество. Поскольку атом выводим из А, каждая полная модель должна принадлежать либо либо но не обоим сразу. Ясно, что если некоторому предложению Си которое принадлежит или выводится из него, присваивает значение ложь, то оно будет ложным для любого элемента из , значит, в нет модели, для которой множество выполнимо. Если найдется подобное предложение которому присваивает значение ложь, то это будет означать, что невыполнимо.

Это и служит целью семантической стратегии очищения. Путем „разумного" выбора резолюций разыскиваются модели для которые исчерпывают весь набор моделей (в смысле для

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

12.5.1. Определения

Дерево Т — это множество узлов с заданным на нем частичным порядком Говорят, что узел расположен непосредственно над узлом если Обратно, узел расположен непосредственно под узлом

Рис. 12.12. Дерево Т.

Упорядочение определяется следующими правилами:

(i) Существует выделенный узел называемый корнем рассматриваемого дерева, для которого нет узла, расположенного непосредственно над ним.

(ii) Каждый узел, отличный от корня, имеет точно один узел, расположенный непосредственно над ним.

(iii) Если узел не расположен непосредственно ни над каким другим узлом, он называется концевым узлом дерева Т.

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

Говорят, что узел расположен над (под) узлом если он расположен непосредственно над (под) или непосредственно над (под) узлом расположенным непосредственно над (под)

На рис. 12.12 изображено дерево

Семантическое дерево Т для множества предложений получается в результате приписывания литералов узлам дерева Т по следующим правилам:

(i) Пустое предложение приписывается корню дерева Т.

(ii) Пусть — множество узлов дерева Т, расположенных непосредственно под узлом а В, — множество литералов, приписанных узлу Значение истинности для интерпретируется как значение истинности конъюнкции содержащихся в нем литералов. Если Т — семантическое дерево, то дизъюнкция множества должна быть тавтологией.

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

Рис. 12.13. Два семантических дерева для

Например, пусть Тогда На рис. 12.13 показаны два семантических дерева для А. Дерево а получено упорядочением атомов в и последующим приписыванием пустого предложения корню, и — двум узлам, расположенным непосредственно под корнем, узлам, расположенным непосредственно под

узлами первого уровня, и т. д. Это дерево удовлетворяет определению семантического дерева, поскольку на любом уровне дизъюнкция присваиваний, относящихся к узлам, расположенным непосредственно под каким-то узлом, имеет вид (), а это тавтология. Более „кустистое" дерево 6 также удовлетворяет определению семантического дерева, так как дизъюнкция присваиваний узлам, расположенным непосредственно под корнем, является тавтологией

Семантическое дерево Т называется конечным деревом конфликта для множества если для каждого узла и множества узлов расположенных непосредственно под выполняются следующие условия:

(i) Каждое множество В литералов, приписанных узлу есть на самом деле единственный литерал L.

(ii) Множество литералов, приписанных узлу есть

(iii) Ни один из литералов, приписанных узлу, расположенному под не принадлежит множеству литералов, приписанных

Рис. 12.14. Конечное дерево конфликта

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