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

Метод резолюции

Принцип резолюции логики предикатов может быть усилен использованием информации о резольвируемых атомах.

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

a) если в резольвенте за обрамленным атомом справа не следует никакой другой атом, то обрамленный атом удаляют,

b) если в резольвенте за обрамленным атомом справа следует какой-либо атом без рамки, то обрамленный атом оставить для последующего анализа,

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

1. Доказать истинность заключения в высказывании: «Существуют студенты, которые любят всех преподавателей. Ни один из студентов не любит невежд. Следовательно, ни один преподаватель не является невеждой».

Решение:

Пусть предметные переменные х и y определены на множестве индивидов. Введем предикаты:

P₁(x):= «быть студентом»,

P₂(y):= «быть преподавателем»,

P₃(x, y):= «x любит y»,

P₄(y):= «быть невеждой».

Тогда формула для записи исходного суждения имеет вид:

1. преобразуем посылки и отрицание заключения к виду ССФ и введем обозначения для формул:

F₁=∃_x(P₁(x)&∀_y(P₂(y)→P₃(x,y)))=∃_x(P₁(x)&∀_y(ØP₂(y)ÚP₃(x,y)))Þправило П3 (и.п.)=

P₁(a)&∀_y (ØP₂(y)∨P₃(a,y))Þправило П5а (и.п.)=∀_y(P₁(a)&(ØP₂(y)∨P₃(a,y))),

F₂=∀_x(P₁(x)→∀_y(P₄(y)→¬P₃(x,y)))=∀_x(ØP₁(x)Ú∀_y(ØP₄(y)Ú¬P₃(x,y)))Þшаг4 приведения к ПНФ=∀_x∀_y(ØP₁(x)ÚØP₄(y)Ú¬P₃(x,y)),

F₃=¬∀_y(P₂(y)→¬P₄(y))=¬∀_y(ØP₂(y)Ú¬P₄(y))Þшаг2 приведения к ПНФ= $_y(Ø(ØP₂(y)Ú¬P₄(y)))= $_y(P₂(y)&P₄(y))Þшаг2 приведения к ССФ=P₂(b)&P₄(b),

2. выпишем множество дизъюнктов посылок и отрицания заключения:

K={P₁(a),(¬P₂(y)∨P₃(a,y)),(¬P₁(x)∨¬P₄(y)∨¬P₃(x,y)),P₂(b),P₄(b)}.

3. выполним подстановку и унификацию дизъюнктов:

= ¬P₂(b)∨P₃(a,b)ÚP₂(b)=¬P₂(b)∨P₃(a,b)- резольвента;

¬P₂(b)∨P₃(a,b)Ú =

¬P₂(b)∨P₃(a,b)Ú =

¬P₂(b)∨P₃(a,b)Ú¬P₁(a)∨¬P₄(b)∨¬P₃(a,b)=¬P₂(b)∨P₃(a,b)Ú¬P₁(a)∨¬P₄(b) –резольвента;

¬P₂(b)∨P₃(a,b)Ú¬P₁(a)∨¬P₄(b)ÚP₁(a)=¬P₂(b)∨P₃(a,b)Ú¬P₁(a)∨¬P₄(b) – резольвента;

¬P₂(b)∨P₃(a,b)Ú¬P₁(a)∨¬P₄(b)Ú P₄(b)=¬P₂(b)∨P₃(a,b)Ú¬P₁(a)∨¬P₄(b) – резольвента;

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

2. Доказать истинность заключения:

"_x(P₃(x)&ØP₁(x)®$_y(P₅(y)&P₄(x,y))), $_x(P₂(x)&P₃(x)&"_y(P₄(x,y)®P₂(y))), "_x(P₂(x)®ØP₁(x))

$_x(P₅(x)&P₂(x))

Решение:

1. преобразуем посылки и отрицание заключения в ССФ и введем обозначения для формул:

F₁="_x(P₃(x)&ØP₁(x)®$_y(P₅(y)&P₄(x,y)))="_x(Ø(P₃(x)&ØP₁(x))Ú$_y(P₅(y)&P₄(x,y)))Þ

шаг4 приведения к ПНФ="_x$_y((ØP₃(x)ÚP₁(x))Ú(P₅(y)&P₄(x,y)))Þ

шаг2б приведения к ССФ="_x((ØP₃(x)ÚP₁(x))Ú(P₅(f(x))&P₄(x,f(x))))=

"_x((ØP₃(x)ÚP₁(x)ÚP₅(f(x)))&(ØP₃(x)ÚP₁(x)ÚP₄(x,f(x))))

F₂=$_x(P₂(x)&P₃(x)&"_y(P₄(x,y)®P₂(y)))=$_x(P₂(x)&P₃(x)&"_y(ØP₄(x,y)ÚP₂(y)))Þ

шаг4 приведения к ПНФ=$_x"_y(P₂(x)&P₃(x)&(ØP₄(x,y)ÚP₂(y)))Þ

шаг2а приведения к ССФ="_y(P₂(а)&P₃(а)&(ØP₄(а,y)ÚP₂(y)))

F₃="_x(P₂(x)®ØP₁(x))="_x(ØP₂(x)ÚØP₁(x))

F₄=Ø$_x(P₅(x)&P₂(x))Þшаг2 приведения к ПНФ="_x(Ø(P₅(x)&P₂(x)))="_x(ØP₅(x)ÚØP₂(x))

2. выпишем множество дизъюнктов:

К={(ØP₃(x)ÚP₁(x)ÚP₅(f(x))),(ØP₃(x)ÚP₁(x)ÚP₄(x,f(x))),P₂(а),P₃(а),(ØP₄(а,y)ÚP₂(y)), (ØP₂(x)ÚØP₁(x)),(ØP₅(x)ÚØP₂(x))}

3. выполним подстановку и унификацию дизъюнктов:

=(ØP₁(a)ÚØP₂(a))ÚP₂(a)= ØP₁(a) – резольвента

ØP₁(a)Ú =ØP₁(a)ÚØP₃(a)ÚP₁(a)ÚP₄(a,f(a))=

ØP₁(a)ÚØP₃(a)ÚP₄(a,f(a)) – резольвента

ØP₁(a)ÚØP₃(a)ÚP₄(a,f(a))Ú

ØP₁(a)ÚØP₃(a)ÚP₄(a,f(a))Ú ØP₄(a,f(a))Ú P₂(f(a))=

ØP₁(a)ÚØP₃(a)ÚP₄(a,f(a))Ú P₂(f(a)) – резольвента

ØP₁(a)ÚØP₃(a)ÚP₄(a,f(a))Ú P₂(f(a))Ú

ØP₁(a)ÚØP₃(a)ÚP₄(a,f(a))Ú P₂(f(a))ÚØP₅(f(a))ÚØP₂(f(a))=

ØP₁(a)ÚØP₃(a)ÚP₄(a,f(a))Ú P₂(f(a))ÚØP₅(f(a)) – резольвента

ØP₁(a)ÚØP₃(a)ÚP₄(a,f(a))Ú P₂(f(a))ÚØP₅(f(a))Ú

ØP₁(a)ÚØP₃(a)ÚP₄(a,f(a))Ú P₂(f(a))ÚØP₅(f(a))ÚØP₃(a)ÚP₁(a)ÚP₅(f(a))Þ

по закону идемпотентности= ØP₁(a)ÚØP₃(a)ÚP₄(a,f(a))ÚP₂(f(a))ÚØP₅(f(a))ÚP₁(a) - резольвента

ØP₁(a)ÚØP₃(a)ÚP₄(a,f(a))ÚP₂(f(a))ÚØP₅(f(a))ÚP₁(a)ÚØP₁(a)=

ØP₁(a)ÚØP₃(a)ÚP₄(a,f(a))ÚP₂(f(a))ÚØP₅(f(a))ÚP₁(a)= ØP₁(a)ÚØP₃(a) – резольвента

ØP₁(a)ÚØP₃(a)ÚP₃(a) – пустая резольвента.

Дата добавления: 2014-01-04