Математическая логика и теория алгоритмов

применяя правила резолюции к дизъюнктам (6) и (7), имеем (8)D. Таким образом, получаем вывод пустого дизъюнкта •. Отметим, что бьши порождены всего три лок-резольвенты. При использовании обычной (неограниченной) резолюции для полу­ чения • были порождены 34 резольвенты. Результативность лок-резолюции не зависит от того, как проиндексировать литеры в S. Введем в рассматриваемом примере индексы иначе, например, так: (1) xP^iQ, (2) 3/ »V4le, ( 3 ) 5 l / ' v , a (4) 7 i Pvg i e , Из (1) и (3) получим: ( 5 ) 2 0 . Аналогично получаем: ( 6 ) 2Svg l e из(1)и(4), (7)6ev4 lQ из(2)и(3), (8)4lQ из (2) и (4), (9) • из (5) и (8). Можно доказать следующую теорему о полноте лок-резолюции. Теорема 3.7. Пусть S ~ множество дизъюнктов, в котором! каждая литера индексирована целым числом. Если 5 противоречиво] (невыполнимо), то имеется лок-вывод пустого дизъюнкта • из S. Все в жизни метод. Андрей Белый § 7. Метод резолюцийд л я хорновских дизъюнктов В общем случае метод резолюций требует больших вычислений. Если дизъюнкты имеют специальный вид, являются так называемыми хорновскими дизъюнктами, то вычисления упрощаются. 100