Метод резолюций и его применение в алгебре высказываний и алгебре предикатов

= .

4. - не единичный дизъюнкт, так как нашли множество рассогласований

 для  :

5. Из  мы найдём, что и

6. Пусть 

=

= .

7. - не единичный дизъюнкт, так как мы нашли множество рассогласований для : . Из мы найдём, что и .

8. Пусть

,

=

=

= .

9. Так как  - единичный дизъюнкт, то есть наиболее общий унификатор для .

Пример 2. Определить, унифицируемо ли множество

1. Пусть  и .

2. - не единичный дизъюнкт, так как мы нашли множество рассогласований для : . Из мы знаем, что и .

3. Пусть 

= .

4. - не единичный дизъюнкт, так как мы нашли множество рассогласований для : .

5. Тем не менее нет  элемента, который был бы переменной. Следовательно, алгоритм унификации  завершается, и мы заключаем,  что  не унифицируемо.

Отметим, что вышеуказанный  алгоритм унификации всегда кончает работу для любого конечного непустого множества выражений, так как иначе породилась бы бесконечная последовательность конечных непустых множеств, обладающая тем свойством, что каждое последующее множество содержит на одну переменную меньше, чем предшествующее ( а именно, содержит , а его не содержит). Но это невозможно, так как содержит только конечно число различных переменных.

Ранее указывалось, что  для унифицируемого алгоритм унификации всегда будет находить наиболее общий унификатор. Это доказывается в следующей теореме.

Теорема унификации. Если - конечное непустое унифицируемое множество выражений, то алгоритм унификации будет всегда кончать работу на шаге 2 и последнее будет наиболее общим унификатором для .

Доказательство. Так как унифицируемо, то обозначим любой его унификатор. Индукцией по  покажем, что существует такая подстановка ,

что . Пусть , положим . Тогда , так как . Предположим теперь, что имеет место для . Если - единичный дизъюнкт, то алгоритм унификации остановится на шаге 2. Так как , то будет наиболее общим унификатором для . Если - не единичный дизъюнкт, то алгоритм унификации будет находить множество рассогласований для . Так как - унификатор для , то должно унифицировать . Однако так как - множество рассогласований, то в должна существовать переменная. Пусть -  любой другой элемент, отличный от . Тогда, так как унифицирует , то . Затем, если встречается в , то встречается в . Однако, это невозможно, так и различны, и . Следовательно, не встречается в . Поэтому алгоритм унификации не остановится на шаге 3, а перейдёт к шагу 4 – к множеству . Пусть . Тогда, так как не встречается в , то .

Таким образом, мы имеем

=

= 

= 

=  .

Значит  = . Следовательно,             .

Поэтому для всех существует такая подстановка , что . Так как алгоритм унификации должен кончить работу и так как он не окончился на шаге 3, то он должен окончиться на шаге 2. Кроме того, так как для всех , то последнее будет наиболее общим унификатором для , что и требовалось доказать.

Введя алгоритм унификации, мы сможем теперь рассмотреть метод  резолюций для логики предикатов.

Если две или более  литер (с одинаковым знаком дизъюнкта) дизъюнкта  имеют наиболее общий унификатор , то называется склейкой . Если - единичный дизъюнкт, то склейка называется единичной склейкой.

Например, пусть  . Тогда первая и вторая литеры имеют наиболее общий унификатор . Следовательно, есть склейка .

Если  и - два дизъюнкта (дизъюнкты – посылки), которые не имеют никаких общих переменных. Пусть и - две литера в и соответственно. Если и имеют наиболее общий унификатор , то дизъюнкт называется (бинарной) резольвентой и . Литеры и называют отрезаемыми литерами.

Пример 1. Пусть  и . Так как входит в и , то мы заменим переменную в и пусть . Выбираем и . Так как , то и имеют наиболее общий унификатор . Следовательно,

=

= .

Таким образом, - бинарная резольвента и . и - отрезаемые литеры.

Резольвентой дизъюнктов – посылок и является одна из следующих резольвент:

1. бинарная резольвента и ;
2. бинарная резольвента и склейки ;
3. бинарная резольвента  и склейки ;
4. бинарная резольвента склейки и склейки .

Пример 2. Пусть  и . Склейка есть . Бинарная резольвента и есть . Следовательно есть резольвента и .

Правило резолюций есть правило вывода, которое порождает  резольвенты для множества дизъюнктов. Это правило было введено в 1965 году Робинсоном. Метод резолюций полон, то есть при помощи правила резолюций для любого невыполнимого множества дизъюнктов можно породить пустой дизъюнкт □. Рассмотрим один пример из планиметрии.

Пример. Показать, что  внутренние накрест лежащие углы, образованные диагональю трапеции, равны.

Чтобы доказать эту теорему, мы сперва аксиоматизируем её. Пусть  обозначает, что - трапеция с верхней левой вершиной  , верхней правой вершиной , нижней правой вершиной и нижней левой вершиной .

 Пусть  обозначает, что отрезок параллелен отрезку , и пусть

  означает, что угол равен углу . Тогда мы имеем следующие аксиомы:   

    определение   

                                                                                            трапеции,

[                        внутренние накрест           

                                        ]               лежащие углы для

                                                                                          параллельных линий  

                                                                                          равны,

                                                                дана на рис.

Из этих аксиом мы должны уметь вывести, что   истинно, то есть

есть истинная формула. Так как мы хотим доказать это  путем опровержения выполнимости, мы отрицаем заключение и докажем, что невыполнимо. Чтобы это сделать, преобразуем выражение в стандартную форму следующим образом:

{

  }. Эта стандартная форма есть множество из четырёх дизъюнктов. Теперь методом резолюций докажем, что множество невыполнимо:

(1)                                дизъюнкт в ,

(2)                       дизъюнкт в ,

(3)                                                       дизъюнкт в ,

(4)                                               дизъюнкт в ,

(5)                                                      резольвента (2) и (4),

(6)                                                      резольвента (1) и (5),

(7)  □                                                                      резольвента (3) и (6).

Так как последний  выведенный из дизъюнкт пустой, то мы заключаем, что невыполнимо.

 

 

 

 

 

 

 

 

 

 

 

          

 Стратегии метода резолюций.

В множестве дизъюнктов существует, как правило, не одна пара дизъюнктов, к которым можно применить правило резолюций. Способ выбора дизъюнктов и литералов в них, к которым применяется правило резолюций (и правило склейки) для получения резольвенты, называется стратегией метода. Рассмотрим три стратегии: стратегия насыщения уровней. Предпочтения более коротких дизъюнктов и вычеркивания.

Стратегия насыщения  уровней. Наиболее простой с идейной точки зрения способ выбора дизъюнктов для получения резольвенты состоит в организации полного перебора возможных вариантов. Этот перебор можно организовать следующим образом. Пусть S₀=S – исходное множество дизъюнктов. Будем считать, что S₀ упорядочено. Пусть D₂ пробегает по порядку множество дизъюнктов S₀, начиная со второго. В качестве D₁ берем последовательно дизъюнкты из S₀, предшествующие D₂ начиная с первого, и формируем последовательность S₁, состоящее из всевозможных резольвент дизъюнктов D₁ и D₂. (Порядок на S₀ определяется порядком добавления дизъюнктов в S₁.) Предположим, что получены последовательности дизъюнктов S₀, S₁,…,S_n-1 и n>1. Тогда последовательность S_n получается следующим образом. В качестве D₂ берутся по порядку дизъюнкты из S_n-1, а в качестве D₁ – дизъюнкты из S₀ S₁ … S_n-1, предшествующие D₂. Последовательность S_n будет состоять из всевозможных резольвент дизъюнктов D₁ и D₂. Процесс порождения резольвент прекращается, как только получается пустой дизъюнкт. Описанная стратегия называется стратегией насыщения уровней. (Уровни – это последовательности S₀, S₁,…,S_n,…) Проследим, как она работает на примере множества дизъюнктов S={X Y, ØXÚØY, X Z, ØXÚZ, ØZ}:

S₀: (1) X Y,                      S₂:  (13) X Y               из (1) и (6),

  (2) ,                         (14)           из (2) и (6),

  (3) X Z,                         (15) X Y               из (1) и (7),

  (4) Z,                         (16)          из (2) и (7),

  (5) ,                                   (17) X Z               из (3) и (7),

S₁: (6) Y       из (1) и (2),   (18) Z            из (4) и (7),

  (7) X      из (1) и (2),  (19) X Z                из (1) и (8),

  (8) Z         из (2) и (3),  (20) Z             из (6) и (8),

  (9) Y Z         из (1) и (3),  (21) Z            из (2) и (9),

  (10) Z              из (3) и (4),  (22) Y Z                из (6) и (9),

  (11) X              из (3) и (5),  (23) Z                      из (8) и (9),

  (12)             из (4) и (5),  (24) □                      из (5) и (10).

Мы видим, что порождено  много лишних дизъюнктов. Так, (6) и (7)–тождественно истинные дизъюнкты. Удаление или добавление тождественно истинного дизъюнкта не влияет на выполнимость множества дизъюнктов, поэтому такие дизъюнкты должны быть удалены из вывода. Далее, некоторые дизъюнкты порождаются неоднократно, например, X Y, ØX ØY, Y Z. Это означает, что выбором дизъюнктов для получения резольвенты надо управлять.

Стратегия предпочтения (более коротких дизъюнктов). Эта стратегия является следующей модификацией предыдущей: сначала в качестве D₂ берется самый короткий дизъюнкт из S_n-1 (если таких несколько, то они перебираются по порядку), затем более длинные и т.д. Аналогичные условия налагаются и на D₁. Такая стратегия в применении к тому же множеству дизъюнктов S дает следующее:

S0: (1) X Y,         S2: (13)        из (2) и (6),

          (2) ,                        (14) Z           из (2) и (6),

          (3) X Z,                         (15) Y           из (1) и (7),

(4) Z,                                 (16) Z            из (3) и (7),

  (5)                                   (17) □            из (6) и (7).

S1: (6) X             из (3) и (5),    

          (7)            из (4) и (5),   

  (8) Y    из (1) и (2),   

  (9) X       из (1) и (2), 

        (10) Z      из (2) и (3),

        (11) Y Z        из (1) и (4),

        (12) Z              из (3) и (4),

Вывод оказался короче, чем  в предыдущем примере, но по-прежнему содержит повторяющиеся и тождественно истинные дизъюнкты. Свободным от этих недостатков является вывод, полученный в соответствие со следующей стратегией.

Стратегия вычеркивания.

 Дизъюнкт D называется расширением дизъюнкта C, если существует подстановка σ такая, что σ(C) D. Для логики высказываний это означает, что просто D=C D (при некоторой перестановке литералов). В случае логики предикатов ситуация не столь проста. Например, D=Q(a) P(b,y) R(u) есть расширение дизъюнкта C=P(x,y) Q(z) Q(v).

Стратегия вычеркивания, как и стратегия предпочтения является модификацией стратегии насыщения уровней. Она применяется следующим образом: после того, как получена очередная резольвента D дизъюнктов D₁ и D₂ проверяется, является ли она тождественно истинной формулой или расширением некоторого дизъюнкта C из S₀ ... S_n-1, и в случае положительного ответа D вычеркивается, т.е. не заносится в последовательность S_n.