Метод резолюций в логике предикатов

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

Подстановка называется унификатором для множества тогда и только тогда, когда ==…=. Говорят, что множество унифицируемо, если для него существует унификатор. Унификатор для множества выражений будет наиболее общим унификатором тогда и только тогда, когда для каждого унификатора для этого множества существует такая подстановка, что =.

Например, множество унифицируемо, так как подстановка является его унификатором.

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

Пусть даны и. Эти два множества не тождественны. Рассогласование в том, что встречается в, а переменная в. Чтобы отождествить и, мы сперва должны найти рассогласование, а затем попытаться его исключить. Для и рассогласование будет. Так как — переменная, то можно заменить на, и таким образом рассогласование будет исключено. В это и заключается идея, на которой и основан алгоритм унификации.

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

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

Алгоритм унификации.

Шаг 1. Множество и .

Шаг 2. Если — единичный дизъюнкт, то остановка — наиболее общий унификатор для. В противном случае найдём множество рассогласований для .

Шаг 3. Если существуют такие элементы и в, что — переменная, не входящая в, то перейти к шагу 4. В противном случае остановка: не унифицируемо.

Шаг 4. Пусть и. (Заметим, что =.).

Шаг 5. Присвоить значение и перейти к шагу 2.

Пример 1. Найти наиболее общий унификатор для.

1. и. Так как — не единичный дизъюнкт, то не является наиболее общим унификатором для .

2. Множество рассогласований. В существует переменная, которая не встречается в .

3. Пусть.

=.

=.

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₀: (1) XY, S₂: (13) XY из (1) и (6),.

• (2), (14) из (2) и (6),
• (3) XZ, (15) XY из (1) и (7),
• (4) Z, (16) из (2) и (7),
• (5), (17) XZ из (3) и (7),

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

• (7) X из (1) и (2), (19) XZ из (1) и (8),
• (8) Z из (2) и (3), (20) Z из (6) и (8),
• (9) YZ из (1) и (3), (21) Z из (2) и (9),
• (10) Z из (3) и (4), (22) YZ из (6) и (9),
• (11) X из (3) и (5), (23) Z из (8) и (9),
• (12) из (4) и (5), (24)? из (5) и (10).

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

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

S0: (1) XY, S2: (13) из (2) и (6),.

• (2), (14) Z из (2) и (6),
• (3) XZ, (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) YZ из (1) и (4),
• (12) Z из (3) и (4),

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

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

Дизъюнкт D называется расширением дизъюнкта C, если существует подстановка у такая, что у (C)D. Для логики высказываний это означает, что просто D=CD (при некоторой перестановке литералов). В случае логики предикатов ситуация не столь проста. Например, 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.

Применение стратегии к прежнему множеству дизъюнктов дает следующее:

S0: (1) XY,.

• (2) ,
• (3) XZ,
• (4) Z,
• (5),

S1: (6) Z из (2) и (3),.

• (7) YZ из (1) и (4),
• (8) Z из (3) и (4),
• (9) X из (3) и (5),
• (10) из (4) и (5),
• (11) из (5) и (6),
• (12) Y из (5) и (7),
• (13)? из (5) и (8).

Рассмотренные стратегии являются полными в том смысле, что если множество дизъюнктов S невыполнимо, то из S пользуясь стратегией можно вывести пустой дизъюнкт. Для первых двух стратегий это достаточно очевидно. Полнота стратегии вычеркивания следует из того, что если D и C-дизъюнкты из S и D — расширение C, то множество S невыполнимо в том и только в том случае, когда невыполнимо множество S{D}.