19. Сколемовские нормальные формы и хорновские дизьюнкты.

Сколемовская нормальная форма – форма, которая состоит из префиксов (кванторов всеобщности) и матрицы, которая представлена в виде конъюнкции дизъюнкции литералов (литерал – атомарная формула с отрицанием или без него).

х₁,х₂, …,х_n p(x₁ … x_n)

^{префикс матрица}

В сколемовской форме префикс можно не писать.

Вместо конъюнкции говорят система предложений (предложение – дизъюнкция литералов).

В соответствие с утверждением, что любая формула логики предикатов может быть представлена в Сколемовской нормальной форме, можно говорить, что любая формула может быть представлена системой предложений.

Дизъюнкт — это дизъюнкция конечного числа литералов. Если дизъюнкт не содержит литералов, его называют пустым дизъюнктом. Хорновские дизъюнкты – дизъюнкты, в которых не больше одного положительного предиката.

_____

22.Метод линейной резолюции.

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

Среди неполных стратегий самая популярная – линейная.

Пример:

Высказывания:

1). Всякий, кто умеет читать – грамотный; 2). Дельфины – не грамотны; 3). Некоторые дельфины обладают интеллектом; Гипотеза: Некоторые, кто не умеет читать, обладают интеллектом.

1).| 1).

2).| 2).

3).&| 3).а) ; б) Д(В)

Н).| 4).

.

. . . . . . . . .

. . . . . . . . .

- гипотеза выводима, т.е. превращается в теорему.

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

Линейная резолюция не полна. Существует пример доказательств, которые не могут быть осуществлены с помощью линейной резолюции.

Линейная резолюция с учетом предков – полна (предки – предыдущие вершины).