Искусственный интеллект

Здесь al%x) , i = 1, ..., и обозначает литерал, такой, что a™ (x) =° at(x), при о/ = 1 и ctfix) =-. аДх,) при af ^= 0. Аналогичный смысл имеет «имвол ej в литерале $f (у), j = 1, ..., п. Подстановка (8(/)) означает формулу, получающуюся из формулы/в результате подстановки 8 во все ее атомы. Суть обобщенного Правила модус лоненс можно выразить следующим образом. Если существует истинная формула а,"1 (х.) v ... v ам-<«> (дсм) v a* (x) v ам<«»» (хм) v... v aM«"- (xj, являющаяся,дизъюнкцией литерадов а°Чх), i = 1,..., п, и истинная формула р," (ух) v... v р\ *•) (уя) v p/(jj) v P^,^"(у„) v... v ря«(yjl, также являющаяся дизъюнкцией литералов fifiy), j = 1, ..., я, и в этих формулах предикатные символы литералов а/" (х) и $^ (у^ одинаковы (at = р\), о/ ^ е/, и для атомов а™ (х,) и р** (к) существует унификация 5, делающая их одинаковыми (записывается как Унификация а.((х), Р/.(>>)) = 6), то можно вывести истинную формулу, получающуюся в результате подстановки 8 в дизъюнкцию исходных формул после удаления в них литералов а™(х) и $? (у). Выведенную таким образом истинную формулу называют резольвентой. Так же как и в случае резолюции для логики высказываний, обобщенную резолюцию можно выразить с использованием импликации.