Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

Литера 2Q и 4Q одна и та же. Так как 2<4, то Q получает индекс 2, поэтому получаем ( 4 ) ^ . Дизъюнкт (4) и является лок-резолъвентой дизъюнктов (1) и (2). Отметим, что если бы литеры в дизъюнкте (2) были индексированы иначе, например, так: {1) 4^ V3Q, ТО литерой в дизъюнкте (2 ), которую разрешено отрезать, была бы 3Q. Однако к iP нельзя применить правило резолюции. Поэтому не существует лок-резольвенты дизъюнктов (1) и (2*). Под лок-резолюцией понимается последовательное получение лок-резольвент из данного множества дизъюнктов и вновь получаемых дизъюнктов. Рассмотрим множество S дизъюнктов, которое введено в §3: Р^, Pv^Q, -iPv-ig. Проведём следующую индексацию: {^)iPV2Q, {2),Pv4^Q, (3) б —P^sQ, (4) 8—>P'^7—>Q- Из дизъюнктов (1) - (4) можно получить только одну лок-резольвенту ( 5 ) ^ ^ из(3)и(4), а из дизъюнктов (1) - (5) только две лок-резольвенты: (6)26 из(1)и(5), (7) 4-.6 из (2) и (5). Применяя правила резолюции к дизъюнктам (6) и (7), имеем: ( 8 ) ^ Таким образом, получаем вывод пустого дизъюнкта => Отметим, что были порождены всего три лок-реолъвенты. При использовании метода исчерпания уровня для получения =^ыли порождены 34 резольвенты. Результативность лок-резолюции не зависит от того, как проиндексировать литеры в S. Введём в рассматриваемом примере индексы иначе, например, так: {^)iPV2Q, {2)ЗРу4 -А (3) 5 —PveQ, {A)J^Pvs^Q. Из (1) и (3) получаем: 67