Представление и обработка знаний

78 Рассмотрим метод линейной резолюции, который был пред- ложен независимо друг от друга Д. Лаврендом и Д. Лакхемом. Линейным выводом из множест- ва дизъюнктов S называется последо- вательность дизъюнктов С 1 , С 2 , ..., С n , в которой C 1 принадлежит S , а каждый член С i+ 1 , i = 1, 2, ..., n – 1, является ре- зольвентой дизъюнктов С i (централь- ный дизъюнкт) и B i (боковой ди- зъюнкт) (рис. 3.4). Боковой дизъюнкт удовлетворяет одному из следующих условий: 1) B i принадлежит S ; 2) B i является некоторым дизъ- юнктом C j , предшествующим в выводе дизъюнкту С i , т.е. j < i . Рассмотрим пример (рис. 3.5): S = { P V R ,  P V R , P V  R ,  P V  R }: Рис. 3.5. Пример линейного вывода В результате линейного вывода получен пустой дизъюнкт. R  R  P V  R P P V  R R  P V R P V R С 1 С 2 B 1 С n B n –1 Центральные дизъюнкты Боковые дизъюнкты Рис. 3.4. Схема линейного вывода