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

РефератПомощь в написанииУзнать стоимостьмоей работы

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

Метод резолюций в логике предикатов (реферат, курсовая, диплом, контрольная)

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

Например, множество:

унифицируемо, так как подстановка:

является его унификатором.

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

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

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

Например, если есть:

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

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

Шаг 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 году Робинсоном. Метод резолюций полон, то есть при помощи правила резолюций для любого невыполнимого множества дизъюнктов можно породить пустой дизъюнкт ?. Рассмотрим один пример из планиметрии.

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

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