Стратегии резолюций методом опровержения

Применение принципа резолюций соответствует последовательному и полному перебору исходных предложений G и получающихся поколений резольвент R¹(G), R²(G) и т. д. Такой перебор, как правило, неприемлем на практике, так как множества R¹(G), R²(G),... слишком быстро разрастаются. Поэтому на практике используют различные стратегии и методы, ускоряющие получение пустой резольвенты.

Стратегия просмотром предложений в ширину. Каждому предложению ставится в соответствие глубина: 0 — для исходных предложений, 1 — для резольвент от них и т. д., n — для резольвент двух предложений, одно из которых (или оба) имеет глубину n-1. Таким образом, резольвенту глубины p можно получить только построив как минимум одну резольвенту глубины р-1. Используя стратегию в ширину для примера на рисунке 9.1 получим следующий граф поиска (рис.9.3) :

P(X)ÚQ(f(X)) ùP(a)ÚR(Z) ùR(b) ùQ(U)

Q(f(a))ÚR(Z) P(X) ùP(a)

Q(f(a)) Q(f(a)) R(Z) R(Z) œ

Рис. 9.3. Граф поиска

Из графа поиска выбираем граф опровержения (рис.9.4).

P(X)ÚQ(f(X)) ùP(a)ÚR(Z) ùR(b) ùQ(U)

P(X) ùP(a)

œ

Рис. 9.4. Граф опровержения

Рассмотренная стратегия является полной и позволяет получить опровержение, т.е. пустое предложение наименьшей глубины.

Стратегия использования опорного множества.Пусть G — невыполнимое множество предложений и Т — подмножество G, такое что множество G-T — выполнимо. Опорным называют множество предложений, которое включает:

1. все предложения подмножества Т;

2. резольвенты тех пар предложений, одно из которых принадлежит опорному множеству.

Таким образом, по меньшей мере один из родителей резольвенты является предложением из опорного множества. Эта стратегия уменьшает граф поиска. Она является полной.

Используя в качестве опорного множества предложение ùR(b) и ùQ(U), получим граф поиска (рис.9.5) и граф опровержения (рис.9.6). Предложения опорного множества на графе поиска подчеркнуты.

ùR(b) ùQ(U) P(X)ÚQ(f(X)) ùP(a)ÚR(Z)

ùP(a)P(X)

Q(f(a))œ

Рис. 9.5. Граф поиска

ùR(b)ùQ(U)P(X)ÚQ(f(X))ùP(a)ÚR(Z)

ùP(a)P(X)

œ

Рис. 9.6. Граф опровержения

В этом примере граф опровержения содержится в графе поиска и совпадает с графом опровержения, построенным с помощью стратегии просмотра в ширину.

Для выбора одного множества предложений Т, делающего множество G-T выполнимым используются три основных способа:

1. Множество Т содержит только положительные литералы. В этом случае множества G-T не может быть пустым : в противном случае найдется интерпретация, которая дает всем литералам множества Т значение И и оно будет моделью G , которое однако невыполнимо. Каждое предложение G-T содержит отрицательный литерал; множество G-T выполнимо, поскольку интерпретация, дающая значение И всем его отрицательным литералам является моделью множества G-T.

2. Множество Т содержит только отрицательные литералы. Выполнимость множества G-T рассматривается аналогично способу 1.

3. Множество Т составляют предложения, полученные из отрицания предположения, которое требуется доказать. В этом случае G-T — это множество аксиом, которое естественно предполагается выполнимым.

Если множество G невыполнимо, то оно должно содержать по меньшей мере одно предложение, включающее все положительные литералы (в противном случае для множества предложений G, каждое из которых включает по меньшей мере один отрицательный литерал, можно было бы построить модель, как указано способом 1). Из этого следует, что применение стратегии опорного множества способом 1 возможно. Аналогично множество G должно содержать по меньшей мере одно предложение со всеми отрицательными литералами, что подтверждается возможностью применения способа 2.