501
Правило резолюции (или резолюция) уже рассматривалось во второй главе. Это правило гласит, что из истинности двух дизъюнкций, одна из которых содержит дизъюнкт, а другая — его отрицание, следует (выводима) формула, являющаяся дизъюнкцией исходных формул без упомянутого дизъюнкта и его отрицания. Резолюция записывалась в следующем виде:
├
или эквивалентно 
├
.
В логике предикатов первого порядка она выглядит так же. Формулы 
в ней являются формулами этой логики. Введем по аналогии с обобщенным правилом модус поненс обобщенное правило резолюции, или обобщенную резолюцию:
,
,
├
Подстановка
.
Здесь 
, i = 1, ..., п обозначает литерал, такой, что = 
, при 
= 1 и = 
при = 0. Аналогичный смысл имеет символ 
в литерале 
, j = 1, ..., m. Подстановка
означает формулу, получающуюся из формулы f в результате подстановки 
во все ее атомы. Суть обобщенного правила модус поненс можно выразить следующим образом. Если существует истинная формула
являющаяся дизъюнкцией литералов , i = 1, ..., п, и истинная формула
также являющаяся дизъюнкцией литералов , j = 1, ..., m, и в этих формулах предикатные символы литералов и одинаковы (
), 
, и для атомов и существует унификация , делающая их одинаковыми (записывается как Унификация 
), то можно вывести истинную формулу, получающуюся в результате подстановки в дизъюнкцию исходных формул после удаления в них литералов и . Выведенную таким образом истинную формулу называют резольвентой. Так же как и в случае резолюции для логики высказываний, обобщенную резолюцию можно выразить с использованием импликации. Обратим внимание, что исходные формулы в обобщенной резолюции и резольвента являются дизъюнкцией литералов. Обычно такие формулы называют клаузальными формами, или клаузами. Таким образом, использование резолюции для вывода требует клаузальной формы представления знаний. Это, в свою очередь, означает, что база знаний, вывод для которой осуществляется на основе обобщенной резолюции, должна представлять собой совокупность клауз, понимаемых в целом как формула, являющаяся конъюнкцией клауз. Формулы такого типа обычно называют конъюнктивными нормальными формулами.
