8.7. МОДЕЛЬНЫЕ СТРАТЕГИИ

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

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

По определению модель не удовлетворяет предложению С, если С имеет константный частный случай (полученный с помощью элементов универсума Эрбрана), принимающий значение при означивании на основе данной модели. В противном случае говорят, что модель удовлетворяет предложению С.

Обычно можно определить непосредственно, удовлетворяет ли данная модель М предложению С. Например, модель не удовлетворяет предложению — так как подстановка приводит к константному частному случаю со значением истинности Эта модель удовлетворяет предложению так как ни одна из подстановок не приводит к константному частному случаю со значением истинности

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

то моделью может быть, например, множество

В терминах атомов эрбрановской базы эта модель представляет собой бесконечное множество

Заметим, что первое и четвертое предложения этой моделью не удовлетворяются, а второе и третье — удовлетворяются.

Понятием модели можно воспользоваться для того, чтобы, ограничить число резольвенций, необходимых для нахождения

Рис. 8.4. (см. скан) Граф опровержения, удовлетворяющий модельной стратегии, в которой используется для определения модели.

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

Теорема 8.2. Пусть — неудовлетворимое множество предложений и М — модель, заданная на его эрбрановской базе. Тогда существует такой граф опровержения для что каждая его вершина либо является предложением из либо имеет

в качестве одной из непосредственно предшествующих ей вершин предложение, которое не удовлетворяется моделью М.

Стратегию, основанную на теореме 8.2, называют модельной стратегией. Критерий, которому должна удовлетворять пара предложений для того, чтобы ее можно было подвергнуть резольвенции в отношении модельной стратегии, таков, что по крайней мере одно из предложений пары не удовлетворяется моделью.

Мы будем обозначать через объединение множества и множества всех резольвент всех пар из допускаемых модельной стратегией. Положим

Согласно теореме 8.2, если множество неудовлетворимо, то найдется такое что

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

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