Правильно построенные формулы (ППФ) и предложения

Правильно построенная формула (ППФ)

–всякий атом есть ППФ

–если G и H – ППФ, а X – переменная, то ( H), (G H), (G H), ( X)G, ( X)H – ППФ.

Предложение – формула, представляющая собой дизъюнкцию литералов

Преобразование ППФ в предложения

Исключение символов эквивалентности и импликации F G (F G) (G F)

F G F G

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

(F G) F G

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

Исключение кванторов существования Например, пусть имеем ( X)( Y) P(X,Y)

Видимо, Y зависит от X, т.е. Y=g(X) (т.н. функция Сколема или сколемовская функция).

Тогда можно записать: ( X)P(X,g(X))

Резольвенты

Пусть имеется два конкретных (не содержащих переменных) предложения P1 P2 … Pn и P1 Q1 … Qm

Из этих двух предложений можно вывести новое предложение, называемое резольвентой или резолюцией. Резольвентой является дизъюнкция этих предложений с последующим исключением пары P1 и P1.

Очевидно, что принцип резолюций покрывает правило вывода modus ponens. Пример. Пусть имеется пара предложений

P R и R Q (или P R, R Q)

Резольвентой этих предложений является P Q (или P Q). Это правило вывода называется сцеплением.

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

унификацией. Пусть имеется пара

F(X) G(X) и F(f(Y)) Если первое предложение заменить наF(f(Y)) G(f(Y)), то получим резольвенту G(f(Y)).

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

Алгоритм опровержения с помощью резолюций

Предположим, что целью алгоритма резолюций является доказательства

G H.

Резолюция(G,H)

1.Сформировать C – множество предложений, полученных путем преобразования формул множества G.

2.Добавить к множеству C предложения, полученные из H.

3.Пока в C не появится пустое предложение выполнять:

•3.1. Выбрать 2 различных предложения S1 и S2 из C.

•3.2. Если они имеют резольвенту R, то добавить эту резольвенту к множеству C.

Конец цикла Конец алгоритма.

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

Пример.

Доказать справедливость рассуждения: «Человек – живое существо. Любое живое существо смертно. Сократ- человек. Следовательно, Сократ смертен».

Граф вывода

человек(X) животное(X)		животное (Y) смертен(Y)

{Y/X}

человек(сократ)		человек(Y) смертен(Y)

{сократ/Y}

смертен(Y)		смертен(сократ)

{сократ/Y}

[]

Пример.

Описание: Любой студент, который сдает экзамен по истории и выигрывает в лотерею

– счастлив. Известно, что любой удачливый или старательный студент может сдать все экзамены. Сидоров не относится к числу старательных студентов, но достаточно удачлив. Любой удачливый студент выигрывает в лотерею.

Вопрос: счастлив ли Сидоров?

Предикатная и дизъюнктивная формы

Исходное	Высказывания предикатов	Дизъюнктивная форма
предложение
Любой студент,	X(pass(X, history) win(X, lottery)	pass(X, history)
который сдает	happy(X))	win(X,lottery) happy(X).
экзамен по
информатике и
выигрывает в
лотерею – счастлив.
Известно, что любой	X Y(study(X) lucky(X)	study(Y) pass(Y,Z).
удачливый или	pass(X,Y))	lucky(Y) pass(Y,Z).
старательный
студент может
сдать все экзамены.
Сидоров не	study(сидоров) lucky(сидоров).	study(сидоров).
относится к числу		lucky(сидоров).
старательных
студентов, но
достаточно удачлив.
Любой удачливый	X(lucky(X) win(X, lottery))	lucky(U) win(U, lottery).
студент
выигрывает в
лотерею.

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

happy(сидоров).

Граф опровержения

pass(X, history) win(X, lottery) happy(X)							lucky(U) win(U, lottery)
		{U/X}
		pass(U, history)		happy(U) lucky(U)					happy(сидоров)
			{сидоров/U}
	lucky(сидоров)				pass(сидоров, history) lucky(сидоров)

	pass(сидоров, history)				lucky(U) pass(U, W)
{сидоров/U, history/W}
			lucky(сидоров)				lucky(сидоров)

[ ]

Граф опровержения разрешения отражает процесс получения противоречия и, следовательно, доказывает, что Сидоров счастлив

Программа доказательства теорем на основе принципа резолюций

Шаг резолюции состоит из следующих действий:

•Берутся 2 предложения в ДНФ D1 и D2.

•Ищутся дизъюнкты P в D1 и P в D2. Если таковые найдены, то формируется дизъюнкция этих предложений с исключением P и P.

•Полученная резольвента добавляется в базу (множество предложений).

Пример унификаторов.

Пусть дано множество литер W = {P(y), P(f(f(z)))}. Приведем ряд подстановок, являющихся унификаторами для W:

= {f(f(a))|y, a|z},= {f(f(z))|y},

= {f(f(f(b)))|y, f(b))|z}.

Подстановка является наиболее общим унификатором для множества W, т.е. НОУ(W) = . Так, например, = ◦ , где = {a|z}, поскольку, в соответствии с определением композиции, имеем множество

{f(f(z)) |y, f(f(a))|y, a|z} = {f(f(a))|y, f(f(a))|y, a|z} = {f(f(a))|y, a|z} = .

Аналогичным образом имеем: = ◦ , где = {f(b)| z}.