Метод резолюций в логике предикатов

Основная идея метода резолюций применительно к формулам логики предикатов та же самая, что и для формул алгебры высказываний. Отличие начинается при нахождении множества дизъюнктов исходной совокупности формул F ₁, F ₂,..., F_m, G, которая проверяется на логическое следование. Каждая формула логики предикатов, которая участвует в доказательстве по методу резолюций, должна быть представлена в специальном стандартном виде. Первый шаг на пути к преобразованию формулы к такому виду – это приведение её к предваренной нормальной форме, бескванторная часть которой приведена к конъюнктивной нормальной форме.

Далее, производится так называемая сколемизация полученной формулы, целью которой является удаление всех кванторов существования, т.е приведение данной формулы к сколемовской нормальной форме

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

 

Примеры выполнения задания

а) Привести к ПНФ следующие формулы.

Пример 1. " X [ P (X) & " y $ X (Ø Q (X, y) ® " z R(A, X, y))].

Решение: Найдём предварённую нормальную форму для формулы:

" X [ P (X) & "y$ X (Ø Q (X, y) ® " z R (A, X, y))] º" X [ P (X) & " y $ X ((Q (X, y) Ú R (A, X, y))] º" X [ P (X) & " y $ T (Q (T, y) Ú R (A, T, y)] º" X [ P (X) & " q $ T (Q (T, q) Ú R (A, T, q))] º" X " q $ T [ P (X) & (Q (T, q) Ú R (A, T, q))].

Пример 2. " x (P (x)↔$ xR (x)) → " yQ (y).

Решение:

Шаг 1.

Шаг 2.

Шаг 3.

Шаг 4. Квантор существования $ z можно вынести за знак дизъюнкции, так как второй член дизъюнкции не зависит от z и может рассматриваться как константа.

Многократно используя этот подход, получаем

.

Пример 3.

Решение:

Шаг 1. Так как выражение не содержит операций импликации и эквивалентности, то нет необходимости в первом шаге.

Шаг 2.

Шаг 3.

Шаг 4.

 

б) Пример 4. Привести следующую формулу к сколемовской форме:

$ u " v $ w " X " y $ z M (u, v, w, X, y, z).

Решение: Формуле $ u " v $ w " X " y $ z M (u, v, w, X, y, z) соответствует сколемовская форма:

" v " X " yM (A, v, F (v), X, y, g (v, X, y)),

где w заменена на F(v) и z – на g(v, X, y) – сколемовские функции.

Пример 5. Найти сколемовскую форму и сколемовские функции для предикатной формулы " X " y $ z $ w " T (Ø S (X, y, y)®(S (z,v, X)& P (w, T, T))), если S (X, y, z)=(X + y = z), P (X, y, z)=(X * y = z) – предикаты суммы и произведения соответственно.

Решение:

1) преобразование импликации:

" X "y$ z $ w " T (S (X,y,y)Ú (S (z,v, X)& P (w, T, T))),

2) Выполним сколемовское преобразование, пусть z = F (X, y), w =g(X, y)

S_A: " X "y " T (S (X, y, y)Ú (S (F (X,y), g(X,y), X) & P (g(X,y), T, T))),

3) Найдём сколемовские функции:

F (X, y) + g (X, y)= X и g (X, y)* T = T, следовательно g (X, y)=1и F (X, y)=1– T.

Пример 6. Привести следующую формулу к сколемовской форме:

" x (($ yP (x, y)→" yQ (x, y))→ R (x)).

Решение: Нормальная формула имеет вид

 

Переименовываем переменную х в кванторе и в области действия этого квантора на z.

В полученной формуле переменную y можно переименовать на w в первой посылке и на u во второй посылке, либо оставить во второй посылке без изменения

Пример 7. Получить СНФ для следующей формулы:

.

Решение: Для получения СНФ вычеркиваем фактор существования $ х и все вхождения переменной х заменяем на константу с поскольку квантору $ х не предшествует ни один квантор всеобщности, то есть сколемовская функция не зависит ни от одной переменной, то есть эта функция является константой.

На следующем шаге вычеркиваем квантор существования $ u и все вхождения переменной u заменяем на функцию f (y, z):

На последнем шаге вычеркиваем квантор $ w.

 

в) Пример 8. Преобразовать в КНФ формулу

Решение: Отрабатываем сначала первое, а потом второе вхождение символов «Ú(».

Здесь чертой подчеркнуты вхождения «Ú(».

Пример 9. Получить множество дизъюнктов для следующей формулы логики предикатов:

(" x){ P (x)Ú[(" y)(P (y)Ú R (x, y))Ù($ y)((Q (x, y)Ú P (y)))]}.

Решение: Первый шаг на пути к преобразованию формулы к такому виду – это приведение её к предваренной нормальной форме, бескванторная часть которой приведена к конъюнктивной нормальной форме.

Применим указанную процедуру к нашей формуле

Далее, произведем сколемизацию полученной формулы, целью которой является удаление всех кванторов существования. Для нашей формулы эта процедура даёт:

Получившиеся дизъюнктивные одночлены образуют множество дизъюнктов исходной формулы, которое, подобно тому как это было в исчислении высказываний, участвует в доказательстве по методу резолюций. Для нашей формулы приходим к следующему множеству дизъюнктов:

 

ТЕМА 8