Кадры, производительность труда, заработная плата

Модификации принципа резолюции (продолжение)
Основные вопросы:
Лок-резолюция
2. Линейная резолюция
3. OL-резолюция
4. Входная резолюция и вывод в языке Пролог
Лок-резолюция
Идея лок-резолюции состоит в использовании индексов для
упорядочения литер в дизъюнктах из данного множества S.
После индексации удалять разрешается только литеры с
наименьшим индексом в каждом из дизъюнктов. Литера наследует свои
индексы из посылок. Если литера наследует более одного индекса, то ей
ставится в соответствие наименьший индекс.
Рассмотрим множество S дизъюнктов,
P∨Q, P∨¬Q, ¬P∨Q, ¬P∨¬Q
Введем индексы, которые будем писать справа вверху от литеры:

Введем следующую индексацию:
P1∨Q2,
P3∨¬Q4,
¬P6∨Q5,
¬P8∨¬Q7
Из дизъюнктов 1-4 можно получить только одну лок-резольвенту
(5) ¬P6 - ЛР(3,4)
Из дизъюнктов 1-5 можно получить только две лок-резольвенты
(6) Q2 - ЛР(1,5)
(7) ¬Q4 - ЛР(2,5)
Применяя правило резолюции к дизъюнктам 6 и 7, получим пустой дизъюнкт
(8) ◻
Результативность лок-резолюции не зависит от того, как проиндексировать литеры в S.
Теорема. Пусть S множество дизъюнктов, в котором каждая литера индексирована целым числом. Если S противоречиво (неудовлетворимо), то имеется лок-вывод пустого дизъюнкта из S

Линейная резолюция
Линейная резолюция довольно легко может быть реализована на ЭВМ, обладает простой структурой и полнотой. Ее частный случай – входная резолюция – является встроенным механизмом дедуктивного вывода в языке логического программирования Пролог.
Линейным выводом из множества дизъюнктов S называется последовательность
дизъюнктов С1, С2, …, Cm, в которой C1 ∈ S, а каждый член Ci+1,
i = 1, 2, …, m-1, является резольвентой дизъюнкта Ci (называемого центральным дизъюнктом) и дизъюнкта Bi, (называемого боковым дизъюнктом), который удовлетворяет одному из двух условий:
Bi ∈ S (i = 1, 2, …, m-1);
2) Bi является некоторым дизъюнктом Cj, предшествующим в выводе
дизъюнкту Ci, т.е. j < i (см. рис.1).

Рис. 1.

П р и м е р 1 . Пусть S = {P ∨ Q, ¬P ∨ Q, P ∨ ¬Q,
¬P ∨ ¬Q}. Тогда линейный вывод пустого дизъюнкта из S
представлен на рис. 2.
Отметим, что из четырех боковых дизъюнктов три
принадлежат S, и только один дизъюнкт Q является
центральным дизъюнктом. Линейная резолюция полна, что
устанавливается следующей теоремой.
Теорема 1. Множество дизъюнктов невыполнимо тогда и только тогда, когда существует линейный вывод пустого дизъюнкта.

Рис. 2.

2. OL-резолюция
Линейная резолюция может быть существенно усилена введением понятия упорядоченного дизъюнкта и использованием информации о резольвированных литерах.
Идея упорядочения дизъюнктов заключается в рассмотрении дизъюнкта как последовательности литер, а не как множества литер.
Отсюда упорядоченным дизъюнктом будем называть дизъюнкт с определенной последовательностью литер.
Говорят, что литера L2 старше литры L1 в упорядоченном дизъюнкте тогда и только тогда, когда L2 следует за L1 в последовательности, определенной упорядоченным дизъюнктом. Отметим, что старшая (наибольшая) литера дизъюнкта является последней литерой дизъюнкта, а младшая литера – первой. Например, в упорядоченном дизъюнкте P(a) ∨ P(b) ∨ P(c)
P(c) является старшей литерой, а P(a) – младшей.

Если две или больше литер (с одинаковыми знаками) упорядоченного дизъюнкта С имеют НОУ σ, то упорядоченный дизъюнкт, полученный из последовательности Сσ вычеркиванием любой литеры, идентичной младшей литере, называется упорядоченным фактором дизъюнкта С.
Пусть имеется упорядоченный дизъюнкт C = P(x) ∨ R(x) ∨ P(a), тогда σ = {a/x} и Cσ = P(a) ∨ R(a) ∨ P(a).
Здесь имеются две идентичные литеры P(a). В соответствии с
определением младшей литерой считается литера, расположенная левее.
Для получения упорядоченного фактора надо из Cσ удалить литеру, идентичную младшей литере. В нашем примере это последняя литера. Следовательно, упорядоченным фактором будет последовательность литер P(a) ∨ R(a).

Отметим, что связывание понятия упорядоченных дизъюнктов с линейной резолюцией не нарушает ее полноты, но существенно увеличивает эффективность метода.
Другим усилением линейной резолюции является использование информации о резольвированных литерах. Обычно при выполнении резолюции образование резольвенты происходит путем удаления резольвированных литер.
Однако оказывается, что эти литеры несут полезную информацию, которая может быть использована для усиления линейной резолюции.
Вернемся к примеру 1. Мы видим, что один из боковых дизъюнктов (дизъюнкт Q) не является входным дизъюнктом. Было бы полезно найти необходимое и достаточное условие, при котором центральный дизъюнкт, полученный ранее, становится боковым.
Дополнительное усиление рассмотренной стратегии было предложено Лавлендом, Ковальским и Кюнером. Ими установлены условия, при которых центральный дизъюнкт может позднее участвовать в роли бокового. Прежде всего, множество литер произвольным образом упорядочивается, т.е. становится известным, какую литеру в дизъюнкте поставить правее, а какую левее. Например, P>Q>R. Тогда упорядоченный дизъюнкт вида P∨Q∨R считается записанным верно, а дизъюнкт R∨P∨Q - нет.
Кроме того, соответствующим образом записывается информация о резольвированных литерах. Вывод, использующий оба эти понятия, называется линейным упорядоченным выводом (OL-выводом (ordered linear deduction)).

Таким образом, при получении редуцируемого упорядоченного дизъюнкта нет необходимости искать, с каким из полученных ранее дизъюнктов он образует линейную резолюцию. Вместо этого можно просто вычеркнуть последнюю литеру в этом упорядоченном дизъюнкте.
Будем называть это вычеркивание операцией редукции.
Операция редукции позволяет не запоминать в OL-выводе промежуточные дизъюнкты. Эта особенность OL-вывода делает его очень удобным при машинной реализации.
Операцию вычеркивания обрамленных литер, за которыми не следуют никакие другие литеры, будем называть операцией сокращения.
Редуцируемый упорядоченный дизъюнкт образуется применением операций редукции и сокращения.
Упорядоченная бинарная резольвента упорядоченных дизъюнктов С1 и
С2 получается конкатенацией последовательностей С1σ и С2σ, где σ есть НОУ для литер L1 и L2 = ¬L1 в С1 и С2 соответственно путем:
1) заключения в рамку L1σ;
2) вычеркивания L2σ;
3) вычеркивания любой необрамленной литеры, которая идентична младшей необрамленной литере последовательности;
4) применение операции сокращения.

Теперь формально определим OL-вывод.
Пусть дано множество упорядоченных дизъюнктов S и упорядоченный дизъюнкт С1 из S. Линейный вывод дизъюнкта Cn из S с начальным дизъюнктом С1 называется OL-выводом, если выполнены следующие
условия:
1) для i = 1, 2, …, n-1, Ci+1 является упорядоченной резольвентой дизъюнкта Ci (называемого центральным упорядоченным дизъюнктом) и дизъюнкта Bi
(называемого боковым упорядоченным дизъюнктом), при этом резольвированная литера в Ci (или в упорядоченном факторе Ci) является последней литерой Ci;
2) Bi является или некоторым дизъюнктом Cj, j < i (если Cj есть редуцируемый упорядоченный дизъюнкт), или дизъюнктом из S (во всех остальных случаях). Если Bi есть некоторый дизъюнкт Cj (j < i), то Ci+1 – редукция дизъюнкта Ci;
3) в выводе нет тавтологий.
Определение упорядоченного дизъюнкта может быть использовано для доказательства следующего утверждения.
В OL-выводе, если Ci есть редуцируемый упорядоченный дизъюнкт, то существует центральный упорядоченный дизъюнкт Cj (j < i), такой, что редукция Ci+1 дизъюнкта Ci является упорядоченной резольвентой Ci с некоторым частым случаем дизъюнкта Cj.

Следующая теорема устанавливает полноту OL-резолюции (Лавленд, Ковальский, Кюнер).
Теорема 2. (о полноте OL-резолюции). Если С является упорядоченным дизъюнктом в невыполнимом множестве упорядоченных дизъюнктов S и если S \ {C} выполнимо, то существует OL-опровержение из S с начальным упорядоченным дизъюнктом С.
Рассмотрим пример реализации OL-резолюции.

или в стандартной форме:
1. ¬C(x) ∨ O(x) ∨ P(f(x));
2. ¬C(x) ∨ O(x) ∨ S(x, f(x));
3. C(a);
4. A(a);
5. ¬S(a, y) ∨ A(y);
6. ¬O(x) ∨ ¬A(x);
7. ¬P(x) ∨ ¬A(x)
Дерево OL-вывода пустого дизъюнкта изображено на Рис. 4.

Рис. 4.

Отметим, что OL-вывод успешно конкурирует со многими резолюционными методами вывода за счет простоты организации поиска.
Простота эта объясняется тем, что не нужно запоминать промежуточные дизъюнкты, а также тем, что здесь всегда определен один из резольвируемых дизъюнктов. OL-вывод – это по существу то же самое, что и метод элиминации моделей, как назвал его Лавленд, или специальный SL-вывод в смысле Ковальского и Кюнера, т.е. разновидность линейной резолюции с функцией выбора (selection function).
Возвращаясь к примеру 1, мы обнаружили, что невозможно построить линейный вывод пустого дизъюнкта, если в качестве боковых дизъюнктов брать только дизъюнкты из исходного множества S (центральный дизъюнкт Q стал боковым).
Назовем дизъюнкты из исходного множества S входными дизъюнктами.
Тогда резолюция, у которой хотя бы один из двух дизъюнктов при резольвировании является входным, называется входной резолюцией.

Входная резолюция проста, эффективна, но в общем случае, к сожалению, как было видно из примера 1, не полна.
Однако она полна для множества так называемых хорновских дизъюнктов.
Дизъюнкт называется хорновским, если он содержит не более, чем одну
положительную литеру. Он имеет в общем случае вид:
¬P1 ∨ ¬ P2 ∨ … ∨ ¬ Pn ∨ Q
или в импликативной форме: P1 & P2 & … & Pn → Q.
Возвращаясь к примеру, в котором детектив должен доказать, что, если горничная сказала правду, то дворецкий солгал, мы видели, что дерево вывода линейно и вывод пустого дизъюнкта был получен с помощью входной резолюции (см. след. слайд).
В этом примере все дизъюнкты из S были хорновскими в отличие от примера 1, где дизъюнкт P ∨ Q – нехорновский

П р и м е р (о детективе) . Горничная сказала, что она видела дворецкого в гостиной. Гостиная находится рядом с кухней. Выстрел раздался на кухне и мог быть услышан во всех близлежащих комната. Дворецкий, обладающий хорошим слухом, сказал, что он не слышал выстрела. Детектив должен доказать, что если горничная сказала правду, то дворецкий солгал.
1. P → Q: если горничная сказала правду, то дворецкий был в гостиной.
2. Q → R: если дворецкий был в гостиной, то он находился рядом с кухней.
3. R → L: если дворецкий был рядом с кухней, то он слышал выстрел.
4. M → ¬L: если дворецкий сказал правду, то он не слышал выстрела.
Требуется доказать, что если горничная сказала правду, то дворецкий солгал, т.е.
P → ¬M.
Представим посылки в КНФ: (¬P ∨ Q) & (¬Q ∨ R) & (¬R ∨ L) & (¬M ∨ ¬L).
Аналогично заключение: ¬P ∨ ¬M.
Имеем следующее множество дизъюнктов:
1. ¬P ∨ Q,
2. ¬Q ∨ R,
3. ¬R ∨ L,
4. ¬M ∨ ¬L,
и отрицание заключения ¬(¬P ∨ ¬M)
5. P,
6. M.
На рис. 5 приведено дерево вывода. Это дерево линейно и вывод пустого дизъюнкта был получен с помощью входной резолюции. В этом примере все дизъюнкты из S были хорновскими в отличие от примера 1, где дизъюнкт P∨Q – нехорновский.

Входная резолюция и вывод в языке Пролог
В языке Пролог используется упорядоченная входная резолюция, т.е. литеры резольвируются в фиксированном порядке строго слева направо.
Иногда систему вывода в языке Пролог называют SLD-резолюцией, т.е. SL-резолюцией для дефинициальных (definite) дизъюнктов, где под дефинициальным дизъюнктом понимают хорновский дизъюнкт.
Логической программой является множество универсально квантифицированных выражений в логике предикатов вида
Q ← P1 & P2 & … & Pn.
Здесь применяется обратная импликативная запись выражения.
Q и Pi (i = 1÷ n ) являются позитивными литерами, причем Q – заголовок дизъюнкта, а конъюнкция Pi – тело.
Очевидно, что множество выражений является множеством хорновских дизъюнктов, которые могут быть трех видов: