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

Это общее правило вывода, пригодное для использования в ис­числении предикатов; оно носит название правила резолюций.

Оно используется для соединения двух формул, если в состав одной из них входит высказывание А, а во вторую – высказывание .

Формулируется правило резолюций следующим образом:

Если истинно Х А и истинно Y , то можно вывести Х Y.

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

Наименование	Резолюция	Цепное правило	Modus ponens
Посылка 1	Х А	® А	А
Посылка 2	Y	А ® Y	А ® Y
Вывод	Х Y	® Y	Y

P ® Q º Q

Из таблицы видно, что правило резолюции можно рассматривать как аналог цепного правила для формул в конъюнктивной нормальной форме. Правило модус поненс также можно считать частным случаем правила резолюций для ложного Х: ХА º А, если Х = F.

< Предыдущая		Следующая >